我有一个文件夹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
中用另一个文件进行了测试,它能够使用该文件的所有功能。 最佳答案
出现此类问题时,即您已定义了模块X
,但未定义X.x
,则应启动顶层并尝试module S = X
来查看X
中到底有什么可用。