utop: Error: Reference to undefined global `Grammar'

Question

我想检查 Coq 语法的信息所以我将 grammar.cma 加载到 utop:

#load "/home/xxx/.opam/system/lib/coq/grammar/grammar.cma";;

但是有一个错误：

Error: Reference to undefined global `Grammar'

Coq 版本：8.5.0 OCaml 版本：4.02.3 最高版本：1.19

Answer 1

我建议您使用 Drop 命令，它实际上可以让您访问 ML 顶层以进行进一步开发。

$ coqtop.byte
Coq < Drop.
#

ocaml