Использовать функцию после сгенерированной извлечением из Coq в Ocaml

У меня есть папка 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, он может использовать все функции этого файла.