從Coq提取生成後使用函數Ocaml

Question

我有一個文件夾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中的另一個文件進行了測試，它能夠使用該文件的所有功能。

Answer 1

當這樣的問題出現了，即你有一個模塊X定義，但沒有定義X.x，你應該開始的頂層，並嘗試module S = X看到什麼是X恰好可用。