Search code examples
ocamlcoqutop

utop: Error: Reference to undefined global `Grammar'

I want to check the info of Coq grammar so I loaded grammar.cma into utop:

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

but there's an error:

Error: Reference to undefined global `Grammar'

Coq version: 8.5.0 OCaml version: 4.02.3 utop version: 1.19

Solution

  • I suggest you use the Drop command, that will actually give you access to a ML toplevel for further development.

    $ coqtop.byte
Coq < Drop.
#

    Documentation for Drop: https://coq.inria.fr/refman/Reference-Manual008.html#hevea_command137