utop: Fehler: Referenz auf nicht definierte globale `Grammar‘

Question

ich die Informationen von Coq Grammatik überprüfen möchten so lud ich grammar.cma in utop:

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

aber es gibt einen Fehler:

Error: Reference to undefined global `Grammar' 

Coq Version: 8.5.0 OCaml Version: 4.02.3 utop Version: 1.19

Answer 1

ich schlage vor, Sie verwenden Sie den Befehl Drop, das wird tatsächlich geben yo Sie haben Zugriff auf eine ML-Toplevel für die weitere Entwicklung.

$ coqtop.byte 
Coq < Drop. 
# 

Dokumentation für Drop: https://coq.inria.fr/refman/Reference-Manual008.html#hevea_command137