Используйте функцию после сгенерированного извлечения из 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,