ocaml - 从 Coq 提取到 Ocaml 生成后使用函数

Question

我有一个文件夹 tmp这是在我从 coq 提取到 ocaml 之后生成的。

~/tmp/cpf0.ml cpf0.mli cpf0.o cpf0.cmi cpf0.cmx cpf0.cmo

main.ml是我用来调用 cpf0 中的一个函数的文件:

let prf = Cpf0.proof;;

我收到一条错误消息 Cpf0.proof是未绑定(bind)的。
我尝试使用:( proof 存在于 Cpf0 中)。

open Cpf0;;
let prf = proof;;

我得到了同样的错误。

Ocaml 链接:ocamlc -I tmp -c main.ml
我不明白为什么它不接受Cpf0 ?

但是open Cpf0;;单独，链接不会给我任何错误。我用 tmp 中的另一个文件进行了测试，它能够使用该文件的所有功能。

Answer 1

当出现此类问题时，即您有一个模块 X已定义，但 X.x没有定义，你应该启动顶层并尝试module S = X查看 X 中的确切内容.