我有一个文件夹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中到底有什么可用。

10-08 20:18