我想检查 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 utop 版本：1.19
问问题
408 次
1 回答
2
我建议您使用该Drop命令，它实际上可以让您访问 ML 顶层以进行进一步开发。
$ coqtop.byte
Coq < Drop.
#
文档Drop：https ://coq.inria.fr/refman/Reference-Manual008.html#hevea_command137
于 2016-04-20T00:16:34.510 回答