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

Question

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

Answer 1

Когда возникает такая проблема, т.е. у вас определен модуль X, но X.x не определен, вы должны запустить уровень и попробовать module S = X, чтобы увидеть, что именно доступно в X.