diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3a57c14a3b..5f982346ab 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -38,9 +38,9 @@ end - dynamic rules declared at the evaluation of Coq files (using e.g. Notation, Infix, or Tactic Notation) - - static rules explicitly defined in files g_*.ml4 + - static rules explicitly defined in files g_*.mlg - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and - VERNAC EXTEND (see e.g. file extratactics.ml4) + VERNAC EXTEND (see e.g. file extratactics.mlg) Note that parsing a Coq document is in essence stateful: the parser needs to recognize commands that start proofs and use a different @@ -170,6 +170,7 @@ module Prim : val ne_string : string Entry.t val ne_lstring : lstring Entry.t val var : lident Entry.t + val bar_cbrace : unit Entry.t end module Constr : |