Use post-generation function by extracting from Coq in Ocaml
I have a folder
that is created after I do an extract from coq to ocaml.
~/tmp/cpf0.ml cpf0.mli cpf0.o cpf0.cmi cpf0.cmx cpf0.cmo
is the file I am using to call one function in
let prf = Cpf0.proof;;
I got an
unbound error . I tried using: (
open Cpf0;; let prf = proof;;
I got the same error.
ocamlc -I tmp -c main.ml
I don't understand why he doesn't accept
, the link does not give me any error. I tested with another file in
, it can use all the functions of this file.
source to share