tmpcoq から ocaml に抽出した後に生成されるフォルダーがあります。
~/tmp/cpf0.ml cpf0.mli cpf0.o cpf0.cmi cpf0.cmx cpf0.cmo
main.mlで 1 つの関数を呼び出すために使用するファイルです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が、そのファイルのすべての機能を使用できます。