CoqからOcamlへの抽出で生成された関数を使用

Question

私はcoqからocamlへの抽出後に生成されるtmpというフォルダを持っています。

~/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の別のファイルでテストしましたが、そのファイルのすべての機能を使用することができます。

Answer 1

このような問題が生じ、すなわち、あなたはXが定義されたモジュールを持っていますが、X.xが定義されていない、あなたはトップレベルを開始し、Xで正確に利用可能であるかを確認するmodule S = Xを試してみてください。