Verwenden Sie die Funktion nach der Extraktion von Coq nach Ocaml generiert

Question

Ich habe einen Ordner tmp, die nach der Extraktion von Coq nach Ocaml generiert wird.

~/tmp/cpf0.ml cpf0.mli cpf0.o cpf0.cmi cpf0.cmx cpf0.cmo 

main.ml ist eine Datei, die ich eine Funktion in cpf0 anrufen verwenden:

let prf = Cpf0.proof;; 

ich einen Fehler bekam sagen Cpf0.proof ungebunden ist. Ich versuchte zu verwenden: (proof existiert in Cpf0).

open Cpf0;; 
let prf = proof;; 

Ich habe den gleichen Fehler.

Ocaml Verknüpfung: ocamlc -I tmp -c main.ml

Ich verstehe nicht, warum es nicht Cpf0 akzeptiert?

Aber open Cpf0;; allein, die Verknüpfung gibt mir keinen Fehler. Ich habe mit einer anderen Datei in tmp getestet, es ist in der Lage, alle Funktionen dieser Datei zu verwenden.

Answer 1

Wenn ein solches Problem auftritt, das heißt Sie haben ein Modul X definiert, aber X.x nicht definiert ist, sollten Sie die Top-Level starten und versuchen module S = X zu sehen, was in X genau zur Verfügung steht.