我有一个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是未绑定的。我尝试使用：（proof存在于Cpf0）。
open Cpf0;;
let prf = proof;;
我得到了同样的错误。
Ocaml 链接：ocamlc -I tmp -c main.ml
我不明白为什么它不接受Cpf0？
但open Cpf0;;仅此而已，链接不会给我任何错误。我用另一个文件进行了测试tmp，它能够使用该文件的所有功能。