Use post-generation function by extracting from Coq in Ocaml

I have a folder tmp

that is created after I do an extract from coq to ocaml.

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

is the file I am using to call one function in cpf0


let prf = Cpf0.proof;;


I got an Cpf0.proof

unbound error . I tried using: ( proof

exists in cpf0


open Cpf0;;
let prf = proof;;


I got the same error.

Ocaml Communication: ocamlc -I tmp -c

I don't understand why he doesn't accept cpf0


But only open Cpf0;;

, the link does not give me any error. I tested with another file in tmp

, it can use all the functions of this file.


source to share

1 answer

When such a problem occurs, i.e. you have a specific module X

but X.x

not defined, you should start filling out and try module S = X

to find out what exactly is available in X




All Articles