CODEWITHSUNDEEP
ocamlcoqutop
Pallar Pak
Pallar Pak

Reputation: 23

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

Upvotes: 2

Views: 483

Answers (1)

ejgallego
ejgallego

Reputation: 6852

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

Upvotes: 3

Related Questions