diff options
| author | Pierre-Marie Pédrot | 2016-11-30 22:47:38 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-11-30 22:47:38 +0100 |
| commit | cf8ecf83b5cc52f7ea73dc1d3af59bf03deff688 (patch) | |
| tree | bd5a6ad80bb09684899fbcc66963d39ae9a9b52a /parsing | |
| parent | 88b2eb9279bf5f83f27057094de5b696ee9916e3 (diff) | |
| parent | 3e6fa1cbdc0ec145728089000595b6ea29f37a4c (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 8 |
2 files changed, 9 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b3233f8f08..d46880831f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -767,6 +767,11 @@ GEXTEND Gram implicit_status = MaximallyImplicit}) items ] ]; + name_or_bang: [ + [ b = OPT "!"; id = name -> + not (Option.is_empty b), id + ] + ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ [ name = name -> [(snd name, Vernacexpr.NotImplicit)] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 77884fb1c7..d987bb4557 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -38,7 +38,7 @@ module Gram : module type of Compat.GrammarMake(CLexer) | (together with a constr entry level, e.g. 50, and indications of) | (subentries, e.g. x in constr next level and y constr same level) | - | spliting into tokens by Metasyntax.split_notation_string + | splitting into tokens by Metasyntax.split_notation_string V [String "x"; String "+"; String "y"] : symbol_token list | @@ -95,7 +95,7 @@ module Gram : module type of Compat.GrammarMake(CLexer) *) -(** Temporary activate camlp4 verbosity *) +(** Temporarily activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -208,14 +208,14 @@ type gram_reinit = gram_assoc * gram_position val grammar_extend : 'a Gram.entry -> gram_reinit option -> 'a Extend.extend_statment -> unit -(** Extend the grammar of Coq, without synchronizing it with the bactracking +(** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) (** {5 Extending the parser with summary-synchronized commands} *) module GramState : Store.S -(** Auxilliary state of the grammar. Any added data must be marshallable. *) +(** Auxiliary state of the grammar. Any added data must be marshallable. *) type 'a grammar_command (** Type of synchronized parsing extensions. The ['a] type should be |