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.ml cpf0.mli cpf0.o cpf0.cmi cpf0.cmx cpf0.cmo

      

        
        
        
      

    

main.ml

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 main.ml

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.