Merge PR #10614: Update the Gallina grammar in doc, "Terms" section

Ack-by: Zimmi48

18 files changed, 2845 insertions, 3643 deletions

diff --git a/Makefile.build b/Makefile.build
index ff0e5dbaea..5b879220d0 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -363,36 +363,6 @@ $(COQPP): $(COQPPCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml coqpp/coqpp_m
 	$(SHOW)'OCAMLC -a $@'
 	$(HIDE)$(OCAMLC) -I coqpp $^ -linkall -o $@
 
-DOC_GRAMCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex))
-
-$(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/tools/docgram/doc_grammar.ml
-	$(SHOW)'OCAMLC -a $@'
-	$(HIDE)$(OCAMLC) -I coqpp $^ -package str -linkall -linkpkg -o $@
-
-DOC_MLGS := */*.mlg plugins/*/*.mlg
-DOC_EDIT_MLGS := doc/tools/docgram/*_mlg
-DOC_RSTS := doc/sphinx/*.rst doc/sphinx/*/*.rst
-
-doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
-	$(SHOW)'DOC_GRAM'
-	$(HIDE)$(DOC_GRAM) -short -no-warn $(DOC_MLGS)
-
-#todo: add a dependency of sphinx on orderedGrammar and of *.rst on orderedGrammar when we're ready
-doc/tools/docgram/orderedGrammar: $(DOC_GRAM) $(DOC_EDIT_MLGS)
-	$(SHOW)'DOC_GRAM_RSTS'
-	$(HIDE)$(DOC_GRAM) $(DOC_MLGS) $(DOC_RSTS)
-
-.PHONY: doc_gram doc_gram_rsts doc_gram_verify
-
-doc_gram: doc/tools/docgram/fullGrammar
-
-doc_gram_verify: doc/tools/docgram/fullGrammar
-	$(SHOW)'DOC_GRAM_VERIFY'
-	$(HIDE)$(DOC_GRAM) -short -no-warn -verify $(DOC_MLGS) $(DOC_RSTS)
-
-#todo: add dependency on $(DOC_RSTS) very soon
-doc_gram_rsts: doc/tools/docgram/orderedGrammar
-
 ###########################################################################
 # Specific rules for Uint63
 ###########################################################################
diff --git a/Makefile.doc b/Makefile.doc
index 041f26f0b4..8e958532f0 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -227,6 +227,45 @@ install-doc-sphinx:
 		$(INSTALLLIB) doc/sphinx/_build/$$d/$$f $(FULLDOCDIR)/sphinx/$$d/$$f;\
 	done; done)
 
+######################################################################
+# doc_grammar tool
+######################################################################
+
+DOC_GRAMCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex))
+
+$(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/tools/docgram/doc_grammar.ml
+	$(SHOW)'OCAMLC -a $@'
+	$(HIDE)$(OCAMLC) -I coqpp $^ -package str -linkall -linkpkg -o $@
+
+# user-contrib/*/*.mlg omitted for now (e.g. ltac2)
+PLUGIN_MLGS := $(wildcard plugins/*/*.mlg)
+OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg
+DOC_MLGS := */*.mlg $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS)))
+DOC_EDIT_MLGS := doc/tools/docgram/*.edit_mlg
+DOC_RSTS := doc/sphinx/*.rst doc/sphinx/*/*.rst
+
+doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
+	$(SHOW)'DOC_GRAM'
+	$(HIDE)$(DOC_GRAM) -short -no-warn $(DOC_MLGS)
+
+#todo: add a dependency of sphinx on updated_rsts when we're ready
+doc/tools/docgram/orderedGrammar doc/tools/docgram/updated_rsts: $(DOC_GRAM) $(DOC_EDIT_MLGS)
+	$(SHOW)'DOC_GRAM_RSTS'
+	$(HIDE)$(DOC_GRAM) $(DOC_MLGS) $(DOC_RSTS)
+
+doc/tools/docgram/updated_rsts: doc/tools/docgram/orderedGrammar
+
+.PHONY: doc_gram doc_gram_verify doc_gram_rsts
+
+doc_gram: doc/tools/docgram/fullGrammar
+
+doc_gram_verify: doc/tools/docgram/fullGrammar
+	$(SHOW)'DOC_GRAM_VERIFY'
+	$(HIDE)$(DOC_GRAM) -short -no-warn -verify $(DOC_MLGS) $(DOC_RSTS)
+
+doc_gram_rsts: doc/tools/docgram/updated_rsts
+
+
 # For emacs:
 # Local Variables:
 # mode: makefile
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index b568160356..45b3f6f161 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -192,7 +192,7 @@ Disjunctive patterns
 --------------------
 
 Multiple patterns that share the same right-hand-side can be
-factorized using the notation :n:`{+| @mult_pattern}`. For
+factorized using the notation :n:`{+| @patterns_comma}`. For
 instance, :g:`max` can be rewritten as follows:
 
 .. coqtop:: in reset
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 0754145b39..7136cc28d1 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -283,7 +283,7 @@ Notice that in the case of type scheme axiom (i.e. whose type is an
 arity, that is a sequence of product finished by a sort), then some type
 variables have to be given (as quoted strings). The syntax is then:
 
-.. cmdv:: Extract Constant @qualid @string ... @string => @string
+.. cmdv:: Extract Constant @qualid {+ @string } => @string
    :undocumented:
 
 The number of type variables is checked by the system. For example:
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 4feda5e875..ca5b5e54a7 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -741,7 +741,7 @@ following grammar:
             : topdown `strategy`         (top-down)
             : hints `ident`              (apply hints from hint database)
             : terms `term` ... `term`      (any of the terms)
-            : eval `redexpr`             (apply reduction)
+            : eval `red_expr`             (apply reduction)
             : fold `term`               (unify)
             : ( `strategy` )
 
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 867a19efe5..f1dd7479c5 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,18 +183,17 @@ todo_include_todos = False
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
-    'tactic',
-    # 142 occurrences currently sort of defined in the ltac chapter,
-    # but is it the right place?
-    'module',
-    'redexpr',
-    'modpath',
-    'dirpath',
     'collection',
+    'command',
+    'dirpath',
+    'modpath',
+    'module',
+    'red_expr',
+    'symbol',
+    'tactic',
     'term_pattern',
     'term_pattern_string',
-    'command',
-    'symbol' ]]
+]]
 
 # -- Options for HTML output ----------------------------------------------
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index a047bab421..ae0afc7819 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -79,14 +79,6 @@ To build an object of type :token:`ident`, one should provide the constructor
        Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
        Check half.
 
-.. FIXME: move this to the main grammar in the spec chapter
-
-.. _record-named-fields-grammar:
-
-  .. productionlist::
-    record_term : {| [`field_def` ; … ; `field_def`] |}
-    field_def : `ident` [`binders`] := `term`
-
 Alternatively, the following syntax allows creating objects by using named fields, as
 shown in this grammar. The fields do not have to be in any particular order, nor do they have
 to be all present if the missing ones can be inferred or prompted for
@@ -163,10 +155,11 @@ available:
 
 .. _record_projections_grammar:
 
-  .. productionlist:: terms
-     projection : `term` `.` ( `qualid` )
-          : `term` `.` ( `qualid` `arg` … `arg` )
-          : `term` `.` ( @`qualid` `term` … `term` )
+  .. insertgram term_projection term_projection
+
+  .. productionlist:: coq
+     term_projection : `term0` .( `qualid` `args_opt` )
+                     : `term0` .( @ `qualid` `term1_list_opt` )
 
   Syntax of Record projections
 
@@ -591,7 +584,7 @@ Advanced recursive functions
 
 The following experimental command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``:
 
-.. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term
+.. cmd:: Function @ident {* @binder} { @fixannot } : @type := @term
 
    This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper
    for several ways of defining a function *and other useful related
@@ -600,16 +593,11 @@ The following experimental command is available when the ``FunInd`` library has
    The meaning of this declaration is to define a function ident,
    similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must
    be given (unless the function is not recursive), but it might not
-   necessarily be *structurally* decreasing. The point of the :n:`{ @decrease_annot }` annotation
+   necessarily be *structurally* decreasing. The point of the :n:`{ @fixannot }` annotation
    is to name the decreasing argument *and* to describe which kind of
    decreasing criteria must be used to ensure termination of recursive
    calls.
 
-   .. productionlist::
-      decrease_annot : struct `ident`
-                     : measure `term` `ident`
-                     : wf `term` `ident`
-
 The ``Function`` construction also enjoys the ``with`` extension to define
 mutually recursive definitions. However, this feature does not work
 for non structurally recursive functions.
@@ -874,7 +862,7 @@ Sections create local contexts which can be shared across multiple definitions.
       :name: Let Fixpoint
       :undocumented:
 
-   .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}
+   .. cmdv:: Let CoFixpoint @ident @fix_body {* with @fix_body}
       :name: Let CoFixpoint
       :undocumented:
 
@@ -2323,6 +2311,18 @@ Printing universes
 Existential variables
 ---------------------
 
+.. insertgram term_evar evar_binding
+
+.. productionlist:: coq
+   term_evar : ?[ `ident` ]
+             : ?[ ?`ident` ]
+             : ?`ident` `evar_bindings_opt`
+   evar_bindings_opt : @{ `evar_bindings_semi` }
+                     : `empty`
+   evar_bindings_semi : `evar_bindings_semi` ; `evar_binding`
+                      : `evar_binding`
+   evar_binding : `ident` := `term`
+
 |Coq| terms can include existential variables which represents unknown
 subterms to eventually be replaced by actual subterms.
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 94e9ccf0d4..3cc101d06b 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -52,7 +52,7 @@ Comments
   They can contain any character. However, embedded :token:`string` literals must be
   correctly closed. Comments are treated as blanks.
 
-Identifiers and field identifiers
+Identifiers
   Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and
   ``'``, that do not start with a digit or ``'``.  That is, they are
   recognized by the following grammar (except that the string ``_`` is reserved;
@@ -60,7 +60,6 @@ Identifiers and field identifiers
 
   .. productionlist:: coq
      ident             : `first_letter`[`subsequent_letter`…`subsequent_letter`]
-     field             : .`ident`
      first_letter      : a..z ∣ A..Z ∣ _ ∣ `unicode_letter`
      subsequent_letter : `first_letter` ∣ 0..9 ∣ ' ∣ `unicode_id_part`
 
@@ -71,10 +70,6 @@ Identifiers and field identifiers
   symbols and non-breaking space. :production:`unicode_id_part`
   non-exhaustively includes symbols for prime letters and subscripts.
 
-  Field identifiers, written :token:`field`, are identifiers prefixed by
-  `.` (dot) with no blank between the dot and the identifier. They are used in
-  the syntax of qualified identifiers.
-
 Numerals
   Numerals are sequences of digits with an optional fractional part
   and exponent, optionally preceded by a minus sign. :token:`int` is an integer;
@@ -144,62 +139,50 @@ presentation of Cic is given in Chapter :ref:`calculusofinductiveconstructions`.
 are given in Chapter :ref:`extensionsofgallina`. How to customize the syntax
 is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
 
-.. productionlist:: coq
-   term             : forall `binders` , `term`
-                    : fun `binders` => `term`
-                    : fix `fix_bodies`
-                    : cofix `cofix_bodies`
-                    : let `ident` [`binders`] [: `term`] := `term` in `term`
-                    : let fix `fix_body` in `term`
-                    : let cofix `cofix_body` in `term`
-                    : let ( [`name` , … , `name`] ) [`dep_ret_type`] := `term` in `term`
-                    : let ' `pattern` [in `term`] := `term` [`return_type`] in `term`
-                    : if `term` [`dep_ret_type`] then `term` else `term`
-                    : `term` : `term`
-                    : `term` <: `term`
-                    : `term` :>
-                    : `term` -> `term`
-                    : `term` `arg` … `arg`
-                    : @ `qualid` [`term` … `term`]
-                    : `term` % `ident`
-                    : match `match_item` , … , `match_item` [`return_type`] with
-                    :   [[|] `equation` | … | `equation`] end
-                    : `qualid`
-                    : `sort`
-                    : `num`
-                    : _
-                    : ( `term` )
-   arg              : `term`
-                    : ( `ident` := `term` )
-   binders          : `binder` … `binder`
-   binder           : `name`
-                    : ( `name` … `name` : `term` )
-                    : ( `name` [: `term`] := `term` )
-                    : ' `pattern`
-   name             : `ident` | _
-   qualid           : `ident` | `qualid` `field`
-   sort             : SProp | Prop | Set | Type
-   fix_bodies       : `fix_body`
-                    : `fix_body` with `fix_body` with … with `fix_body` for `ident`
-   cofix_bodies     : `cofix_body`
-                    : `cofix_body` with `cofix_body` with … with `cofix_body` for `ident`
-   fix_body         : `ident` `binders` [`annotation`] [: `term`] := `term`
-   cofix_body       : `ident` [`binders`] [: `term`] := `term`
-   annotation       : { struct `ident` }
-   match_item       : `term` [as `name`] [in `qualid` [`pattern` … `pattern`]]
-   dep_ret_type     : [as `name`] `return_type`
-   return_type      : return `term`
-   equation         : `mult_pattern` | … | `mult_pattern` => `term`
-   mult_pattern     : `pattern` , … , `pattern`
-   pattern          : `qualid` `pattern` … `pattern`
-                    : @ `qualid` `pattern` … `pattern`
-                    : `pattern` as `ident`
-                    : `pattern` % `ident`
-                    : `qualid`
-                    : _
-                    : `num`
-                    : ( `pattern` | … | `pattern` )
+.. insertgram term binders_opt
 
+.. productionlist:: coq
+   term : forall `open_binders` , `term`
+        : fun `open_binders` => `term`
+        : `term_let`
+        : if `term` `as_return_type_opt` then `term` else `term`
+        : `term_fix`
+        : `term100`
+   term100 : `term_cast`
+           : `term10`
+   term10 : `term1` `args`
+          : @ `qualid` `universe_annot_opt` `term1_list_opt`
+          : `term1`
+   args : `args` `arg`
+        : `arg`
+   arg : ( `ident` := `term` )
+       : `term1`
+   term1_list_opt : `term1_list_opt` `term1`
+                  : `empty`
+   empty :
+   term1 : `term_projection`
+         : `term0` % `ident`
+         : `term0`
+   args_opt : `args`
+            : `empty`
+   term0 : `qualid` `universe_annot_opt`
+         : `sort`
+         : `numeral`
+         : `string`
+         : _
+         : `term_evar`
+         : `term_match`
+         : ( `term` )
+         : {| `fields_def` |}
+         : `{ `term` }
+         : `( `term` )
+         : ltac : ( `ltac_expr` )
+   fields_def : `field_def` ; `fields_def`
+              : `field_def`
+              : `empty`
+   field_def : `qualid` `binders_opt` := `term`
+   binders_opt : `binders`
+               : `empty`
 
 Types
 -----
@@ -213,6 +196,13 @@ of types inside the syntactic class :token:`term`.
 Qualified identifiers and simple identifiers
 --------------------------------------------
 
+.. insertgram qualid field
+
+.. productionlist:: coq
+   qualid : `qualid` `field`
+          : `ident`
+   field : .`ident`
+
 *Qualified identifiers* (:token:`qualid`) denote *global constants*
 (definitions, lemmas, theorems, remarks or facts), *global variables*
 (parameters or axioms), *inductive types* or *constructors of inductive
@@ -220,11 +210,15 @@ types*. *Simple identifiers* (or shortly :token:`ident`) are a syntactic subset
 of qualified identifiers. Identifiers may also denote *local variables*,
 while qualified identifiers do not.
 
-Numerals
---------
+Field identifiers, written :token:`field`, are identifiers prefixed by
+`.` (dot) with no blank between the dot and the identifier.
+
 
-Numerals have no definite semantics in the calculus. They are mere
-notations that can be bound to objects through the notation mechanism
+Numerals and strings
+--------------------
+
+Numerals and strings have no predefined semantics in the calculus. They are
+merely notations that can be bound to objects through the notation mechanism
 (see Chapter :ref:`syntaxextensionsandinterpretationscopes` for details).
 Initially, numerals are bound to Peano’s representation of natural
 numbers (see :ref:`datatypes`).
@@ -243,6 +237,35 @@ numbers (see :ref:`datatypes`).
 Sorts
 -----
 
+.. insertgram sort universe_level
+
+.. productionlist:: coq
+   sort : Set
+        : Prop
+        : SProp
+        : Type
+        : Type @{ _ }
+        : Type @{ `universe` }
+   universe : max ( `universe_exprs_comma` )
+            : `universe_expr`
+   universe_exprs_comma : `universe_exprs_comma` , `universe_expr`
+                        : `universe_expr`
+   universe_expr : `universe_name` `universe_increment_opt`
+   universe_name : `qualid`
+                 : Set
+                 : Prop
+   universe_increment_opt : + `num`
+                          : `empty`
+   universe_annot_opt : @{ `universe_levels_opt` }
+                      : `empty`
+   universe_levels_opt : `universe_levels_opt` `universe_level`
+                       : `empty`
+   universe_level : Set
+                  : Prop
+                  : Type
+                  : _
+                  : `qualid`
+
 There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set`  and :g:`Type`.
 
 -  :g:`SProp` is the universe of *definitionally irrelevant
@@ -266,6 +289,35 @@ More on sorts can be found in Section :ref:`sorts`.
 Binders
 -------
 
+.. insertgram open_binders exclam_opt
+
+.. productionlist:: coq
+   open_binders : `names` : `term`
+                : `binders`
+   names : `names` `name`
+         : `name`
+   name : _
+        : `ident`
+   binders : `binders` `binder`
+           : `binder`
+   binder : `name`
+          : ( `names` : `term` )
+          : ( `name` `colon_term_opt` := `term` )
+          : { `name` }
+          : { `names` `colon_term_opt` }
+          : `( `typeclass_constraints_comma` )
+          : `{ `typeclass_constraints_comma` }
+          : ' `pattern0`
+          : ( `name` : `term` | `term` )
+   typeclass_constraints_comma : `typeclass_constraints_comma` , `typeclass_constraint`
+                               : `typeclass_constraint`
+   typeclass_constraint : `exclam_opt` `term`
+                        : { `name` } : `exclam_opt` `term`
+                        : `name` : `exclam_opt` `term`
+   exclam_opt : !
+              : `empty`
+
+
 Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix`
 *bind* variables. A binding is represented by an identifier. If the binding
 variable is not used in the expression, the identifier can be replaced by the
@@ -291,8 +343,8 @@ the case of a single sequence of bindings sharing the same type (e.g.:
 
 .. index:: fun ... => ...
 
-Abstractions
-------------
+Abstractions: fun
+-----------------
 
 The expression :n:`fun @ident : @type => @term` defines the
 *abstraction* of the variable :token:`ident`, of type :token:`type`, over the term
@@ -313,8 +365,8 @@ Section :ref:`let-in`).
 
 .. index:: forall
 
-Products
---------
+Products: forall
+----------------
 
 The expression :n:`forall @ident : @type, @term` denotes the
 *product* of the variable :token:`ident` of type :token:`type`, over the term :token:`term`.
@@ -359,6 +411,14 @@ Section :ref:`explicit-applications`).
 Type cast
 ---------
 
+.. insertgram term_cast term_cast
+
+.. productionlist:: coq
+   term_cast : `term10` <: `term`
+             : `term10` <<: `term`
+             : `term10` : `term`
+             : `term10` :>
+
 The expression :n:`@term : @type` is a type cast expression. It enforces
 the type of :token:`term` to be :token:`type`.
 
@@ -384,6 +444,22 @@ guess the missing piece of information.
 Let-in definitions
 ------------------
 
+.. insertgram term_let names_comma
+
+.. productionlist:: coq
+   term_let : let `name` `colon_term_opt` := `term` in `term`
+            : let `name` `binders` `colon_term_opt` := `term` in `term`
+            : let `single_fix` in `term`
+            : let `names_tuple` `as_return_type_opt` := `term` in `term`
+            : let ' `pattern` := `term` `return_type_opt` in `term`
+            : let ' `pattern` in `pattern` := `term` `return_type` in `term`
+   colon_term_opt : : `term`
+                  : `empty`
+   names_tuple : ( `names_comma` )
+               : ()
+   names_comma : `names_comma` , `name`
+               : `name`
+
 :n:`let @ident := @term in @term’`
 denotes the local binding of :token:`term` to the variable
 :token:`ident` in :token:`term`’. There is a syntactic sugar for let-in
@@ -392,8 +468,60 @@ stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
 
 .. index:: match ... with ...
 
-Definition by case analysis
----------------------------
+Definition by cases: match
+--------------------------
+
+.. insertgram term_match record_pattern
+
+.. productionlist:: coq
+   term_match : match `case_items_comma` `return_type_opt` with `or_opt` `eqns_or_opt` end
+   case_items_comma : `case_items_comma` , `case_item`
+                    : `case_item`
+   return_type_opt : `return_type`
+                   : `empty`
+   as_return_type_opt : `as_name_opt` `return_type`
+                      : `empty`
+   return_type : return `term100`
+   case_item : `term100` `as_name_opt` `in_opt`
+   as_name_opt : as `name`
+               : `empty`
+   in_opt : in `pattern`
+          : `empty`
+   or_opt : |
+          : `empty`
+   eqns_or_opt : `eqns_or`
+               : `empty`
+   eqns_or : `eqns_or` | `eqn`
+           : `eqn`
+   eqn : `patterns_comma_list_or` => `term`
+   patterns_comma_list_or : `patterns_comma_list_or` | `patterns_comma`
+                          : `patterns_comma`
+   patterns_comma : `patterns_comma` , `pattern`
+                  : `pattern`
+   pattern : `pattern10` : `term`
+           : `pattern10`
+   pattern10 : `pattern1` as `name`
+             : `pattern1_list`
+             : @ `qualid` `pattern1_list_opt`
+             : `pattern1`
+   pattern1_list : `pattern1_list` `pattern1`
+                 : `pattern1`
+   pattern1_list_opt : `pattern1_list`
+                     : `empty`
+   pattern1 : `pattern0` % `ident`
+            : `pattern0`
+   pattern0 : `qualid`
+            : {| `record_patterns_opt` |}
+            : _
+            : ( `patterns_or` )
+            : `numeral`
+            : `string`
+   patterns_or : `patterns_or` | `pattern`
+               : `pattern`
+   record_patterns_opt : `record_patterns_opt` ; `record_pattern`
+                       : `record_pattern`
+                       : `empty`
+   record_pattern : `qualid` := `pattern`
 
 Objects of inductive types can be destructured by a case-analysis
 construction called *pattern matching* expression. A pattern matching
@@ -403,11 +531,11 @@ to apply specific treatments accordingly.
 This paragraph describes the basic form of pattern matching. See
 Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description
 of the general form. The basic form of pattern matching is characterized
-by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a
+by a single :token:`case_item` expression, a :token:`patterns_comma` restricted to a
 single :token:`pattern` and :token:`pattern` restricted to the form
 :n:`@qualid {* @ident}`.
 
-The expression match ":token:`term`:math:`_0` :token:`return_type` with
+The expression match ":token:`term`:math:`_0` :token:`return_type_opt` with
 :token:`pattern`:math:`_1` => :token:`term`:math:`_1` :math:`|` … :math:`|`
 :token:`pattern`:math:`_n` => :token:`term`:math:`_n` end" denotes a
 *pattern matching* over the term :token:`term`:math:`_0` (expected to be
@@ -417,10 +545,10 @@ expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid`
 :token:`ident` where :token:`qualid` must denote a constructor. There should be
 exactly one branch for every constructor of :math:`I`.
 
-The :token:`return_type` expresses the type returned by the whole match
+The :token:`return_type_opt` expresses the type returned by the whole match
 expression. There are several cases. In the *non dependent* case, all
-branches have the same type, and the :token:`return_type` is the common type of
-branches. In this case, :token:`return_type` can usually be omitted as it can be
+branches have the same type, and the :token:`return_type_opt` is the common type of
+branches. In this case, :token:`return_type_opt` can usually be omitted as it can be
 inferred from the type of the branches [2]_.
 
 In the *dependent* case, there are three subcases. In the first subcase,
@@ -520,8 +648,30 @@ Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`).
    single: fix
    single: cofix
 
-Recursive functions
--------------------
+Recursive and co-recursive functions: fix and cofix
+---------------------------------------------------
+
+.. insertgram term_fix term1_extended_opt
+
+.. productionlist:: coq
+   term_fix : `single_fix`
+            : `single_fix` with `fix_bodies` for `ident`
+   single_fix : fix `fix_body`
+              : cofix `fix_body`
+   fix_bodies : `fix_bodies` with `fix_body`
+              : `fix_body`
+   fix_body : `ident` `binders_opt` `fixannot_opt` `colon_term_opt` := `term`
+   fixannot_opt : `fixannot`
+                : `empty`
+   fixannot : { struct `ident` }
+            : { wf `term1_extended` `ident` }
+            : { measure `term1_extended` `ident_opt` `term1_extended_opt` }
+   term1_extended : `term1`
+                  : @ `qualid` `universe_annot_opt`
+   ident_opt : `ident`
+             : `empty`
+   term1_extended_opt : `term1_extended`
+                      : `empty`
 
 The expression “``fix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:``
 :token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` ``with … with``
@@ -547,6 +697,8 @@ syntax: :n:`let fix @ident @binders := @term in` stands for
 The Vernacular
 ==============
 
+.. insertgramXX vernac ident_opt2
+
 .. productionlist:: coq
    decorated-sentence : [ `decoration` … `decoration` ] `sentence`
    sentence           : `assumption`
@@ -568,7 +720,7 @@ The Vernacular
    ind_body           : `ident` [`binders`] : `term` :=
                       : [[|] `ident` [`binders`] [:`term`] | … | `ident` [`binders`] [:`term`]]
    fixpoint           : Fixpoint `fix_body` with … with `fix_body` .
-                      : CoFixpoint `cofix_body` with … with `cofix_body` .
+                      : CoFixpoint `fix_body` with … with `fix_body` .
    assertion          : `assertion_keyword` `ident` [`binders`] : `term` .
    assertion_keyword  : Theorem | Lemma
                       : Remark | Fact
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index e37f300915..b2b426ada5 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -127,7 +127,7 @@ mode but it can also be used in toplevel definitions as shown below.
                      : gfail [`natural`] [`message_token` ... `message_token`]
                      : fresh [ `component` … `component` ]
                      : context `ident` [`term`]
-                     : eval `redexpr` in `term`
+                     : eval `red_expr` in `term`
                      : type of `term`
                      : constr : `term`
                      : uconstr : `term`
@@ -986,9 +986,9 @@ Computing in a constr
 
 Evaluation of a term can be performed with:
 
-.. tacn:: eval @redexpr in @term
+.. tacn:: eval @red_expr in @term
 
-   where :n:`@redexpr` is a reduction tactic among :tacn:`red`, :tacn:`hnf`,
+   where :n:`@red_expr` is a reduction tactic among :tacn:`red`, :tacn:`hnf`,
    :tacn:`compute`, :tacn:`simpl`, :tacn:`cbv`, :tacn:`lazy`, :tacn:`unfold`,
    :tacn:`fold`, :tacn:`pattern`.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index e87b76b4ab..89b24ea8a3 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -195,7 +195,7 @@ Requests to the environment
       (see Section :ref:`invocation-of-tactics`).
 
 
-.. cmd:: Eval @redexpr in @term
+.. cmd:: Eval @red_expr in @term
 
    This command performs the specified reduction on :n:`@term`, and displays
    the resulting term with its type. The term to be reduced may depend on
@@ -1146,7 +1146,7 @@ described first.
       Print all the currently non-transparent strategies.
 
 
-.. cmd:: Declare Reduction @ident := @redexpr
+.. cmd:: Declare Reduction @ident := @red_expr
 
    This command allows giving a short name to a reduction expression, for
    instance ``lazy beta delta [foo bar]``. This short name can then be used
@@ -1158,7 +1158,7 @@ described first.
    functor applications will be rejected if these declarations are not
    local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but
    nothing prevents the user from also performing a
-   :n:`Ltac @ident := @redexpr`.
+   :n:`Ltac @ident := @red_expr`.
 
    .. seealso:: :ref:`performingcomputations`
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 02910e603a..dbe714c388 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -871,7 +871,7 @@ notations are given below. The optional :production:`scope` is described in
                  : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
                  : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
                  : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
-                 : CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`].
+                 : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
                  : [Local] Declare Custom Entry `ident`.
    decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]].
    modifiers     : `modifier`, … , `modifier`
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 98fdc38ca7..a0a1809133 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -186,6 +186,9 @@ that appear in the specified production:
 | WITH <newprod>
 ```
 
+* `PRINT` <nonterminal> - prints the nonterminal definition at that point in
+  applying the edits.  Most useful when the edits get a bit complicated to follow.
+
 * (any other nonterminal name) - adds a new production (and possibly a new nonterminal)
 to the grammar.
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index ea94e21ff3..06b49a0a18 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -12,41 +12,10 @@
 
 DOC_GRAMMAR
 
-(* additional nts to be spliced *)
-
-LEFTQMARK: [
-| "?"
-]
-
-SPLICE: [
-| LEFTQMARK
-]
-
-hyp: [
-| var
-]
-
-tactic_then_gen: [
-| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
-| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
-]
-
-SPLICE: [
-| hyp
-| identref
-| pattern_ident (* depends on previous LEFTQMARK splice todo: improve *)
-| constr_eval  (* splices as multiple prods *)
-| tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
-| Prim.name
-| ltac_selector
-| Constr.ident
-| tactic_then_locality  (* todo: cleanup *)
-| attribute_list
-]
-
+(* renames to eliminate qualified names
+   put other renames at the end *)
 RENAME: [
   (* map missing names for rhs *)
-| _binders binders
 | Constr.constr term
 | Constr.constr_pattern constr_pattern
 | Constr.global global
@@ -54,58 +23,52 @@ RENAME: [
 | Constr.lconstr_pattern lconstr_pattern
 | G_vernac.query_command query_command
 | G_vernac.section_subset_expr section_subset_expr
-| nonsimple_intropattern intropattern
 | Pltac.tactic tactic
-| Pltac.tactic_expr ltac_expr
+| Pltac.tactic_expr tactic_expr5
 | Prim.ident ident
 | Prim.reference reference
 | Pvernac.Vernac_.main_entry vernac_control
 | Tactic.tactic tactic
-| tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
-| tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
-| tactic0 ltac_expr0  (* todo: can't figure out how this gets mapped by coqpp *)
-| tactic_expr5 ltac_expr
-| tactic_expr4 ltac_expr4
-| tactic_expr3 ltac_expr3
-| tactic_expr2 ltac_expr2
-| tactic_expr1 ltac_expr1
-| tactic_expr0 ltac_expr0
-
-  (* elementary renaming/OCaml-defined productions *)
-| clause clause_dft_concl
-| in_clause' in_clause
-| l_constr lconstr  (* todo: should delete the production *)
 
   (* SSR *)
+(*
 | G_vernac.def_body def_body
 | Pcoq.Constr.constr term
 | Prim.by_notation by_notation
 | Prim.identref ident
 | Prim.natural natural
+*)
 | Vernac.rec_definition rec_definition
 
-  (* rename on lhs *)
-| intropatterns intropattern_list_opt
 | Constr.closed_binder closed_binder
+]
 
-  (* historical name *)
-| constr term
+(* written in OCaml *)
+impl_ident_head: [
+| "{" ident
 ]
 
+lpar_id_coloneq: [
+| "(" ident; ":="
+]
+
+(* lookahead symbols *)
 DELETE: [
 | check_for_coloneq
-| impl_ident_head
 | local_test_lpar_id_colon
 | lookup_at_as_comma
 | only_starredidentrefs
 | test_bracket_ident
-| test_lpar_id_coloneq
+| test_lpar_id_colon
+| test_lpar_id_coloneq  (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *)
 | test_lpar_id_rpar
 | test_lpar_idnum_coloneq
+| test_nospace_pipe_closedcurly
 | test_show_goal
 
   (* SSR *)
 (* | ssr_null_entry *)
+(*
 | ssrtermkind  (* todo: rename as "test..." *)
 | term_annotation  (* todo: rename as "test..." *)
 | test_idcomma
@@ -122,48 +85,410 @@ DELETE: [
 | test_ident_no_do
 | ssrdoarg  (* todo: this and the next one should be removed from the grammar? *)
 | ssrseqdir
+*)
+
+(* unused *)
+| constr_comma_sequence'
+| auto_using'
+| constr_may_eval
 ]
 
-ident: [
-| DELETE IDENT ssr_null_entry
+(* ssrintrosarg: [ | DELETENT ] *)
+
+(* additional nts to be spliced *)
+
+hyp: [
+| var
 ]
 
-natural: [
-| DELETE _natural
+empty: [
+|
 ]
 
+or_opt: [
+| "|"
+| empty
+]
 
-  (* added productions *)
+ltac_expr_opt: [
+| tactic_expr5
+| empty
+]
 
-empty: [  (* todo: (bug) this is getting converted to empty -> empty *)
-|
+ltac_expr_opt_list_or: [
+| ltac_expr_opt_list_or "|" ltac_expr_opt
+| ltac_expr_opt
 ]
 
-lpar_id_coloneq: [
-| "(" IDENT; ":="
+tactic_then_gen: [
+| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
+| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
+| REPLACE OPT tactic_expr5 ".." tactic_then_last
+| WITH ltac_expr_opt ".." or_opt ltac_expr_opt_list_or
 ]
 
-name_colon: [
-| IDENT; ":"
-| "_" ":"  (* todo: should "_" be a keyword or an identifier? *)
+ltac_expr_opt_list_or: [
+| ltac_expr_opt_list_or "|" OPT tactic_expr5
+| OPT tactic_expr5
 ]
 
-int: [ (* todo: probably should be NUMERAL *)
-| integer
+reference: [ | DELETENT ]
+
+reference: [
+| qualid
 ]
 
-command_entry: [
-| noedit_mode
+fullyqualid: [ | DELETENT ]
+
+fullyqualid: [
+| qualid
+]
+
+
+field: [ | DELETENT ]
+
+field: [
+| "." ident
+]
+
+basequalid: [
+| REPLACE ident fields
+| WITH qualid field
+]
+
+fields: [ | DELETENT ]
+
+dirpath: [
+| REPLACE ident LIST0 field
+| WITH ident
+| dirpath field
 ]
 
 binders: [
 | DELETE Pcoq.Constr.binders  (* todo: not sure why there are 2 "binders:" *)
 ]
 
-(* edits to simplify *)
+lconstr: [
+| DELETE l_constr
+]
+
+let_type_cstr: [
+| DELETE OPT [ ":" lconstr ]
+| rec_type_cstr
+]
+
+as_name_opt: [
+| "as" name
+| empty
+]
+
+(* rename here because we want to use "return_type" for something else *)
+RENAME: [
+| return_type as_return_type_opt
+]
+
+as_return_type_opt: [
+| REPLACE OPT [ OPT [ "as" name ] case_type ]
+| WITH as_name_opt case_type
+| empty
+]
+
+case_item: [
+| REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
+| WITH operconstr100 as_name_opt OPT [ "in" pattern200 ]
+]
+
+as_dirpath: [
+| DELETE OPT [ "as" dirpath ]
+| "as" dirpath
+| empty
+]
+
+binder_constr: [
+| MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
+| MOVETO term_let "let" single_fix "in" operconstr200
+| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
+| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
+]
+
+term_let: [
+| REPLACE "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
+| WITH "let" name let_type_cstr ":=" operconstr200 "in" operconstr200
+| "let" name LIST1 binder let_type_cstr ":=" operconstr200 "in" operconstr200
+(* Don't need to document that "( )" is equivalent to "()" *)
+| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| WITH "let" [ "(" LIST1 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| REPLACE "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
+| WITH  "let" "'" pattern200 ":=" operconstr200 OPT case_type "in" operconstr200
+| DELETE "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
+]
+
+atomic_constr: [
+(* @Zimmi48: "string" used only for notations, but keep to be consistent with patterns *)
+(* | DELETE string *)
+| REPLACE "?" "[" ident "]"
+| WITH "?[" ident "]"
+| MOVETO term_evar "?[" ident "]"
+| REPLACE "?" "[" pattern_ident "]"
+| WITH "?[" pattern_ident "]"
+| MOVETO term_evar "?[" pattern_ident "]"
+| MOVETO term_evar pattern_ident evar_instance
+]
+
+tactic_expr0: [
+| REPLACE "[" ">" tactic_then_gen "]"
+| WITH "[>" tactic_then_gen "]"
+]
+
+operconstr100: [
+| MOVETO term_cast operconstr99 "<:" operconstr200
+| MOVETO term_cast operconstr99 "<<:" operconstr200
+| MOVETO term_cast operconstr99 ":" operconstr200
+| MOVETO term_cast operconstr99 ":>"
+]
+
+operconstr10: [
+(* fixme: add in as a prodn somewhere *)
+| MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref
+| DELETE dangling_pattern_extension_rule
+]
+
+operconstr9: [
+(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
+| DELETE ".." operconstr0 ".."
+]
+
+arg_list: [
+| arg_list appl_arg
+| appl_arg
+]
+
+arg_list_opt: [
+| arg_list
+| empty
+]
+
+operconstr1: [
+| REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
+| WITH operconstr0 ".(" global arg_list_opt ")"
+| MOVETO term_projection operconstr0 ".(" global arg_list_opt ")"
+| MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
+]
+
+operconstr0: [
+(* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
+| DELETE "{" binder_constr "}"
+]
+
+single_fix: [
+| DELETE fix_kw fix_decl
+| "fix" fix_decl
+| "cofix" fix_decl
+]
+
+fix_kw: [ | DELETENT ]
+
+binders_fixannot: [
+(*
+| REPLACE impl_name_head impl_ident_tail binders_fixannot
+| WITH impl_name_head impl_ident_tail "}" binders_fixannot
+*)
+(* Omit this complex detail.  See https://github.com/coq/coq/pull/10614#discussion_r344118146 *)
+| DELETE impl_name_head impl_ident_tail binders_fixannot
+
+| DELETE fixannot
+| DELETE binder binders_fixannot
+| DELETE (* empty *)
+
+| LIST0 binder OPT fixannot
+]
 
-ltac_expr1: [
+impl_ident_tail: [
+| DELETENT
+(*
+| REPLACE "}"
+| WITH empty
+| REPLACE LIST1 name ":" lconstr "}"
+| WITH LIST1 name ":" lconstr
+| REPLACE LIST1 name "}"
+| WITH LIST1 name
+| REPLACE ":" lconstr "}"
+| WITH ":" lconstr
+*)
+]
+
+of_type_with_opt_coercion: [
+| DELETE ":>" ">"
+| DELETE ":" ">" ">"
+| DELETE ":" ">"
+]
+
+binder: [
+| DELETE name
+]
+
+open_binders: [
+| REPLACE name LIST0 name ":" lconstr
+| WITH LIST1 name ":" lconstr
+(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
+| DELETE name ".." name
+| REPLACE name LIST0 name binders
+| WITH LIST1 binder
+| DELETE closed_binder binders
+]
+
+closed_binder: [
+| name
+
+| REPLACE "(" name LIST1 name ":" lconstr ")"
+| WITH "(" LIST1 name ":" lconstr ")"
+| DELETE "(" name ":" lconstr ")"
+
+| DELETE "(" name ":=" lconstr ")"
+| REPLACE "(" name ":" lconstr ":=" lconstr ")"
+| WITH "(" name rec_type_cstr ":=" lconstr ")"
+
+| DELETE "{" name LIST1 name "}"
+
+| REPLACE "{" name LIST1 name ":" lconstr "}"
+| WITH "{" LIST1 name rec_type_cstr "}"
+| DELETE "{" name ":" lconstr  "}"
+]
+
+typeclass_constraint: [
+| EDIT ADD_OPT "!" operconstr200
+]
+
+(* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*)
+Prim.name: [
+| REPLACE "_"
+| WITH name
+]
+
+oriented_rewriter: [
+| REPLACE orient_rw rewriter
+| WITH orient rewriter
+]
+
+DELETE: [
+| orient_rw
+]
+
+pattern1_list: [
+| pattern1_list pattern1
+| pattern1
+]
+
+pattern1_list_opt: [
+| pattern1_list
+| empty
+]
+
+pattern10: [
+| REPLACE pattern1 LIST1 pattern1
+| WITH LIST1 pattern1
+| REPLACE "@" reference LIST0 pattern1
+| WITH "@" reference pattern1_list_opt
+]
+
+pattern0: [
+| REPLACE "(" pattern200 ")"
+| WITH "(" LIST1 pattern200 SEP "|" ")"
+| DELETE "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
+]
+
+patterns_comma: [
+| patterns_comma "," pattern100
+| pattern100
+]
+
+patterns_comma_list_or: [
+| patterns_comma_list_or "|" patterns_comma
+| patterns_comma
+]
+
+eqn: [
+| REPLACE LIST1 mult_pattern SEP "|" "=>" lconstr
+| WITH patterns_comma_list_or "=>" lconstr
+]
+
+record_patterns: [
+| REPLACE record_pattern ";" record_patterns
+| WITH record_patterns ";" record_pattern
+]
+
+(* todo: binders should be binders_opt *)
+
+
+(* lexer stuff *)
+bigint: [
+| DELETE NUMERAL
+| num
+]
+
+ident: [
+| DELETENT
+]
+
+IDENT: [
+| ident
+]
+
+integer: [ | DELETENT ]
+RENAME: [
+| integer int (* todo: review uses in .mlg files, some should be "natural" *)
+]
+
+LEFTQMARK: [
+| "?"
+]
+
+natural: [ | DELETENT ]
+natural: [
+| num  (* todo: or should it be "nat"? *)
+]
+
+NUMERAL: [
+| numeral
+]
+
+(* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *)
+
+string: [ | DELETENT ]
+STRING: [
+| string
+]
+
+
+(* todo: is "bigint" useful?? *)
+(* todo: "check_int" in g_prim.mlg should be "check_num" *)
+
+  (* added productions *)
+
+name_colon: [
+| name ":"
+]
+
+command_entry: [
+| noedit_mode
+]
+
+tactic_expr1: [
 | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
+| MOVETO ltac_match_goal match_key OPT "reverse" "goal" "with" match_context_list "end"
+| MOVETO ltac_match_term match_key tactic_expr5 "with" match_list "end"
+]
+
+DELETE: [
+| tactic_then_locality
+]
+
+tactic_expr4: [
+| REPLACE tactic_expr3 ";" tactic_then_gen "]"
+| WITH tactic_expr3 ";" "[" tactic_then_gen "]"
+| tactic_expr3 ";" "[" ">" tactic_then_gen "]"
 ]
 
 match_context_list: [
@@ -180,35 +505,37 @@ match_list: [
 | EDIT ADD_OPT "|" LIST1 match_rule SEP "|"
 ]
 
+match_rule: [
+| REPLACE match_pattern "=>" tactic_expr5
+| WITH [ match_pattern | "_" ] "=>" tactic_expr5
+| DELETE "_" "=>" tactic_expr5
+]
+
 
 selector_body: [
 | REPLACE range_selector_or_nth  (* depends on whether range_selector_or_nth is deleted first *)
 | WITH LIST1 range_selector SEP ","
 ]
 
-range_selector_or_nth: [
-| DELETENT
-]
+range_selector_or_nth: [ | DELETENT ]
 
 simple_tactic: [
 | DELETE "intros"
 | REPLACE "intros" ne_intropatterns
-| WITH "intros" intropattern_list_opt
+| WITH "intros" intropatterns
 | DELETE "eintros"
 | REPLACE "eintros" ne_intropatterns
-| WITH "eintros" intropattern_list_opt
+| WITH "eintros" intropatterns
 ]
 
-intropattern_list_opt: [
+intropatterns: [
 | DELETE LIST0 intropattern
-| intropattern_list_opt intropattern
+| intropatterns intropattern
 | empty
 ]
 
-
-ne_intropatterns: [
-| DELETENT  (* todo: don't use DELETENT for this *)
-]
+(* todo: don't use DELETENT for this *)
+ne_intropatterns: [ | DELETENT ]
 
 
 or_and_intropattern: [
@@ -216,5 +543,181 @@ or_and_intropattern: [
 | DELETE "(" simple_intropattern ")"
 | REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")"
 |   WITH  "(" LIST0 simple_intropattern SEP "," ")"
-| EDIT "[" USE_NT intropattern_or LIST1 intropattern_list_opt SEP "|" "]"
+| EDIT "[" USE_NT intropattern_or LIST1 intropatterns SEP "|" "]"
 ]
+
+bar_cbrace: [
+| REPLACE "|" "}"
+| WITH "|}"
+]
+
+(* todo: is this really correct? Search for "Pvernac.register_proof_mode" *)
+(* consider tactic_command vs tac2mode *)
+vernac_aux: [
+| tactic_mode "."
+]
+
+SPLICE: [
+| noedit_mode
+| command_entry
+| bigint
+| match_list
+| match_context_list
+| IDENT
+| LEFTQMARK
+| natural
+| NUMERAL
+| STRING
+| hyp
+| var
+| identref
+| pattern_ident
+| constr_eval  (* splices as multiple prods *)
+| tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
+| Prim.name
+| ltac_selector
+| Constr.ident
+| attribute_list
+| operconstr99
+| operconstr90
+| operconstr9
+| operconstr8
+| pattern200
+| pattern99
+| pattern90
+| ne_lstring
+| ne_string
+| lstring
+| basequalid
+| fullyqualid
+| global
+| reference
+| bar_cbrace
+| lconstr
+| impl_name_head
+
+(*
+| ast_closure_term
+| ast_closure_lterm
+| ident_no_do
+| ssrterm
+| ssrtacarg
+| ssrtac3arg
+| ssrtclarg
+| ssrhyp
+| ssrhoi_hyp
+| ssrhoi_id
+| ssrindex
+| ssrhpats
+| ssrhpats_nobs
+| ssrfwdid
+| ssrmovearg
+| ssrcasearg
+| ssrrwargs
+| ssrviewposspc
+| ssrpatternarg
+| ssr_elsepat
+| ssr_mpat
+| ssrunlockargs
+| ssrcofixfwd
+| ssrfixfwd
+| ssrhavefwdwbinders
+| ssripats_ne
+| ssrparentacarg
+| ssrposefwd
+*)
+
+| preident
+| lpar_id_coloneq
+| binders
+| casted_constr
+| check_module_types
+| constr_pattern
+| decl_sep
+| function_rec_definition_loc (* loses funind annotation *)
+| glob
+| glob_constr_with_bindings
+| id_or_meta
+| lconstr_pattern
+| lglob
+| ltac_tacdef_body
+| mode
+| mult_pattern
+| open_constr
+| option_table
+| record_declaration
+| register_type_token
+| tactic
+| uconstr
+| impl_ident_head
+| argument_spec
+| at_level
+| branches
+| check_module_type
+| decorated_vernac
+| ext_module_expr
+| ext_module_type
+| pattern_identref
+| test
+| binder_constr
+| atomic_constr
+| let_type_cstr
+| name_colon
+| closed_binder
+| binders_fixannot
+]
+
+RENAME: [
+| clause clause_dft_concl
+| in_clause' in_clause
+
+| tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic0 ltac_expr0  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic_expr5 ltac_expr
+| tactic_expr4 ltac_expr4
+| tactic_expr3 ltac_expr3
+| tactic_expr2 ltac_expr2
+| tactic_expr1 ltac_expr1
+| tactic_expr0 ltac_expr0
+
+(* | nonsimple_intropattern intropattern (* ltac2 *) *)
+| intropatterns intropattern_list_opt
+
+| operconstr200 term   (* historical name *)
+| operconstr100 term100
+| operconstr10 term10
+| operconstr1 term1
+| operconstr0 term0
+| pattern100 pattern
+| match_constr term_match
+(*| impl_ident_tail impl_ident*)
+| ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *)
+
+| tactic_then_gen multi_goal_tactics
+| selector only_selector
+| selector_body selector
+| input_fun fun_var
+| match_hyps match_hyp
+
+| BULLET bullet
+| nat_or_var num_or_var
+| fix_decl fix_body
+| instance universe_annot_opt
+| rec_type_cstr colon_term_opt
+| fix_constr term_fix
+| constr term1_extended
+| case_type return_type
+| appl_arg arg
+| record_patterns record_patterns_opt
+| universe_increment universe_increment_opt
+| rec_definition fix_definition
+| corec_definition cofix_definition
+| record_field_instance field_def
+| record_fields_instance fields_def
+| evar_instance evar_bindings_opt
+| inst evar_binding
+]
+
+
+(* todo: ssrreflect*.rst ref to fix_body is incorrect *)
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index eb86bab37e..70976e705e 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -48,6 +48,9 @@ let default_args = {
   verify = false;
 }
 
+let start_symbols = ["vernac_toplevel"]
+let tokens = [ "bullet"; "ident"; "int"; "num"; "numeral"; "string" ]
+
 (* translated symbols *)
 
 type doc_symbol =
@@ -128,8 +131,8 @@ module DocGram = struct
     g_update_prods g nt' (oprods @ nprods)
 
   (* add a new nonterminal after "ins_after" None means insert at the beginning *)
-  let g_add_after g ins_after nt prods =
-    if NTMap.mem nt !g.map then raise Duplicate;  (* don't update the nt if it's already present *)
+  let g_add_after g ?(update=true) ins_after nt prods =
+    if (not update) && NTMap.mem nt !g.map then raise Duplicate;  (* don't update the nt if it's already present *)
     let rec insert_nt order res =
       match ins_after, order with
       | None, _ -> nt :: order
@@ -143,6 +146,11 @@ module DocGram = struct
     g := { order = insert_nt !g.order [];
            map = NTMap.add nt prods !g.map }
 
+  let g_add_prod_after g ins_after nt prod =
+    let prods = try NTMap.find nt !g.map with Not_found -> [] in
+    (* todo: add check for duplicates *)
+    g_add_after g ~update:true ins_after nt (prods @ [prod])
+
   (* replace the map and order *)
   let g_reorder g map order =
     let order_nts = StringSet.of_list order in
@@ -188,13 +196,13 @@ let rec output_prod plist need_semi = function
     | Slist0sep (sym, sep) -> sprintf "LIST0 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep])
     | Sopt sym -> sprintf "OPT %s" (prod_to_str ~plist [sym])
     | Sparen sym_list -> sprintf "( %s )" (prod_to_str sym_list)
-    | Sprod sym_list ->
+    | Sprod sym_list_list ->
       sprintf "[ %s ]" (String.concat " " (List.mapi (fun i r ->
           let prod = (prod_to_str r) in
           let sep = if i = 0 then "" else
               if prod <> "" then "| " else "|" in
           sprintf "%s%s" sep prod)
-        sym_list))
+        sym_list_list))
     | Sedit s -> sprintf "%s" s
     (* todo: make PLUGIN info output conditional on the set of prods? *)
     | Sedit2 ("PLUGIN", plugin) ->
@@ -213,6 +221,8 @@ let rec output_prod plist need_semi = function
 
 and prod_to_str_r plist prod =
   match prod with
+  | Sterm s :: Snterm "ident" :: tl when List.mem s ["?"; "."] && plist ->
+    (sprintf "%s`ident`" s) :: (prod_to_str_r plist tl)
   | p :: tl ->
     let need_semi =
       match prod with
@@ -258,6 +268,15 @@ and output_sep sep =
 
 and prod_to_prodn prod = String.concat " " (List.map output_prodn prod)
 
+let pr_prods nt prods = (* duplicative *)
+  Printf.printf "%s: [\n" nt;
+  List.iter (fun prod ->
+      let str = prod_to_str ~plist:false prod in
+      let pfx = if str = "" then "|" else "| " in
+      Printf.printf "%s%s\n" pfx str)
+    prods;
+  Printf.printf "]\n\n"
+
 type fmt = [`MLG | `PRODLIST | `PRODN ]
 
 (* print a subset of the grammar with nts in the specified order *)
@@ -313,6 +332,8 @@ let cvt_ext prod =
  in
  List.map from_ext prod
 
+let keywords = ref StringSet.empty
+
 let rec cvt_gram_sym = function
   | GSymbString s -> Sterm s
   | GSymbQualid (s, level) ->
@@ -352,6 +373,10 @@ and cvt_gram_sym_list l =
     (Sedit2 ("NOTE", s2)) :: cvt_gram_sym_list tl
   | GSymbQualid ("USE_NT", _) :: GSymbQualid (s2, l) :: tl ->
     (Sedit2 ("USE_NT", s2)) :: cvt_gram_sym_list tl
+  | GSymbString s :: tl ->
+    (* todo: not seeing "(bfs)" here for some reason *)
+    keywords := StringSet.add s !keywords;
+    cvt_gram_sym (GSymbString s) :: cvt_gram_sym_list tl
   | hd :: tl ->
     cvt_gram_sym hd :: cvt_gram_sym_list tl
   | [] -> []
@@ -453,6 +478,7 @@ let plugin_regex = Str.regexp "^plugins/\\([a-zA-Z0-9_]+\\)/"
 
 let read_mlg is_edit ast file level_renames symdef_map =
   let res = ref [] in
+  let locals = ref StringSet.empty in
   let add_prods nt prods =
     if not is_edit then
       add_symdef nt file symdef_map;
@@ -478,6 +504,8 @@ let read_mlg is_edit ast file level_renames symdef_map =
           let len = List.length ent.gentry_rules in
           List.iteri (fun i rule ->
               let nt = ent.gentry_name in
+              if not (List.mem nt grammar_ext.gramext_globals) then
+                locals := StringSet.add nt !locals;
               let level = (get_label rule.grule_label) in
               let level = if level <> "" then level else
                 match ent.gentry_pos with
@@ -528,7 +556,7 @@ let read_mlg is_edit ast file level_renames symdef_map =
   in
 
   List.iter prod_loop ast;
-  List.rev !res
+  List.rev !res, !locals
 
 let dir s = "doc/tools/docgram/" ^ s
 
@@ -536,7 +564,8 @@ let read_mlg_edit file =
   let fdir = dir file in
   let level_renames = ref StringMap.empty in (* ignored *)
   let symdef_map = ref StringMap.empty in (* ignored *)
-  read_mlg true (parse_file fdir) fdir level_renames symdef_map
+  let prods, _ = read_mlg true (parse_file fdir) fdir level_renames symdef_map in
+  prods
 
 let add_rule g nt prods file =
   let ent = try NTMap.find nt !g.map with Not_found -> [] in
@@ -555,9 +584,12 @@ let read_mlg_files g args symdef_map =
   let last_autoloaded = List.hd (List.rev autoloaded_mlgs) in
   List.iter (fun file ->
     (* does nt renaming, deletion and splicing *)
-    let rules = read_mlg false (parse_file file) file level_renames symdef_map in
+    let rules, locals = read_mlg false (parse_file file) file level_renames symdef_map in
     let numprods = List.fold_left (fun num rule ->
         let nt, prods = rule in
+        if NTMap.mem nt !g.map && (StringSet.mem nt locals) &&
+            StringSet.cardinal (StringSet.of_list (StringMap.find nt !symdef_map)) > 1 then
+          warn "%s: local nonterminal '%s' already defined\n" file nt;
         add_rule g nt prods file;
         num + List.length prods)
       0 rules
@@ -572,18 +604,74 @@ let read_mlg_files g args symdef_map =
   !level_renames
 
 
+ (* get the nt's in the production, preserving order, don't worry about dups *)
+ let nts_in_prod prod =
+  let rec traverse = function
+  | Sterm s -> []
+  | Snterm s -> if List.mem s tokens then [] else [s]
+  | Slist1 sym
+  | Slist0 sym
+  | Sopt sym
+    -> traverse sym
+  | Slist1sep (sym, sep)
+  | Slist0sep (sym, sep)
+    -> traverse sym @ (traverse sep)
+  | Sparen sym_list -> List.concat (List.map traverse sym_list)
+  | Sprod sym_list_list -> List.concat (List.map (fun l -> List.concat (List.map traverse l)) sym_list_list)
+  | Sedit _
+  | Sedit2 _ -> []
+  in
+  List.rev (List.concat (List.map traverse prod))
+
+let get_refdef_nts g =
+  let rec get_nts_r refd defd bindings =
+    match bindings with
+    | [] -> refd, defd
+    | (nt, prods) :: tl ->
+      get_nts_r (List.fold_left (fun res prod ->
+                  StringSet.union res (StringSet.of_list (nts_in_prod prod)))
+                refd prods)
+        (StringSet.add nt defd) tl
+   in
+   let toks = StringSet.of_list tokens in
+   get_nts_r toks toks (NTMap.bindings !g.map)
+
+
 (*** global editing ops ***)
 
-let create_edit_map edits =
+let create_edit_map g op edits =
   let rec aux edits map =
     match edits with
     | [] -> map
     | edit :: tl ->
       let (key, binding) = edit in
+      let all_nts_ref, all_nts_def = get_refdef_nts g in
+      (match op with
+      (* todo: messages should tell you which edit file causes the error *)
+      | "SPLICE" ->
+        if not (StringSet.mem key all_nts_def) then
+          error "Undefined nt `%s` in SPLICE\n" key
+      | "DELETE" ->
+        if not (StringSet.mem key all_nts_ref || (StringSet.mem key all_nts_def)) then
+          error "Unused/undefined nt `%s` in DELETE\n" key;
+      | "RENAME" ->
+        if not (StringSet.mem key all_nts_ref || (StringSet.mem key all_nts_def)) then
+          error "Unused/undefined  nt `%s` in RENAME\n" key;
+(*      todo: could not get the following codeto type check
+        (match binding with
+        | _ :: Snterm new_nt :: _ ->
+          if not (StringSet.mem new_nt all_nts_ref) then
+            error "nt `%s` already exists in %s\n" new_nt op
+        | _ -> ())
+*)
+      | _ -> ());
       aux tl (StringMap.add key binding map)
   in
   aux edits StringMap.empty
 
+let remove_Sedit2 p =
+  List.filter (fun sym -> match sym with | Sedit2 _ -> false | _ -> true) p
+
 (* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *)
 let rec edit_prod g top edit_map prod =
   let edit_nt edit_map sym0 nt =
@@ -596,8 +684,8 @@ let rec edit_prod g top edit_map prod =
           try let splice_prods = NTMap.find nt !g.map in
             match splice_prods with
             | [] -> assert false
-            | [p] -> List.rev p
-            | _ -> [Sprod splice_prods]
+            | [p] -> List.rev (remove_Sedit2 p)
+            | _ -> [Sprod (List.map remove_Sedit2 splice_prods)]
           with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt]
         end
       | _ -> [Snterm binding]
@@ -654,16 +742,22 @@ and edit_rule g edit_map nt rule =
 
 (*** splice: replace a reference to a nonterminal with its definition ***)
 
-(* todo: create a better splice routine, handle recursive case *)
+(* todo: create a better splice routine *)
 let apply_splice g splice_map =
-  StringMap.iter (fun nt b ->
-      if not (NTMap.mem nt !g.map) then
-        error "Unknown nt '%s' for apply_splice\n" nt)
-    splice_map;
   List.iter (fun b ->
-      let (nt, prods) = b in
-      let (nt', prods) = edit_rule g splice_map nt prods in
-      g_update_prods g nt' prods)
+      let (nt0, prods0) = b in
+      let rec splice_loop nt prods cnt =
+        let max_cnt = 10 in
+        let (nt', prods') = edit_rule g splice_map nt prods in
+        if cnt > max_cnt then
+          error "Splice for '%s' not done after %d iterations\n" nt0 max_cnt;
+        if nt' = nt && prods' = prods then
+          (nt', prods')
+        else
+          splice_loop nt' prods' (cnt+1)
+      in
+      let (nt', prods') = splice_loop nt0 prods0 0 in
+      g_update_prods g nt' prods')
     (NTMap.bindings !g.map);
   List.iter (fun b ->
       let (nt, op) = b in
@@ -678,7 +772,7 @@ let find_first edit prods nt =
   let rec find_first_r edit prods nt i =
     match prods with
     | [] ->
-      error "Can't find '%s' in REPLACE for '%s'\n" (prod_to_str edit) nt;
+      error "Can't find '%s' in edit for '%s'\n" (prod_to_str edit) nt;
       raise Not_found
     | prod :: tl ->
       if ematch prod edit then i
@@ -906,7 +1000,7 @@ let edit_all_prods g op eprods =
             op (prod_to_str eprod) num;
         aux tl res
     in
-    let map = create_edit_map (aux eprods []) in
+    let map = create_edit_map g op (aux eprods []) in
     if op = "SPLICE" then
       apply_splice g map
     else (* RENAME/DELETE *)
@@ -960,6 +1054,13 @@ let edit_single_prod g edit0 prods nt =
   in
   edit_single_prod_r edit0 prods nt []
 
+let report_undef_nts g prod rec_nt =
+  let nts = nts_in_prod prod in
+  List.iter (fun nt ->
+      if not (NTMap.mem nt !g.map) && not (List.mem nt tokens) && nt <> rec_nt then
+        error "Undefined nonterminal `%s` in edit: %s\n" nt (prod_to_str prod))
+    nts
+
 let apply_edit_file g edits =
   List.iter (fun b ->
       let (nt, eprod) = b in
@@ -970,11 +1071,26 @@ let apply_edit_file g edits =
           | (Snterm "DELETE" :: oprod) :: tl ->
             aux tl (remove_prod oprod prods nt) add_nt
           | (Snterm "DELETENT" :: _) :: tl ->  (* note this doesn't remove references *)
+            if not (NTMap.mem nt !g.map) then
+              error "DELETENT for undefined nonterminal `%s`\n" nt;
             g_remove g nt;
             aux tl prods false
+          | (Snterm "MOVETO" :: Snterm nt2 :: oprod) :: tl ->
+            g_add_prod_after g (Some nt) nt2 oprod;
+            let prods' = (try
+              let posn = find_first oprod prods nt in
+              let prods = insert_after posn [[Snterm nt2]] prods in  (* insert new prod *)
+              remove_prod oprod prods nt      (* remove orig prod *)
+              with Not_found -> prods)
+            in
+            aux tl prods' add_nt
+          | (Snterm "PRINT" :: _) :: tl ->
+            pr_prods nt (NTMap.find nt !g.map);
+            aux tl prods add_nt
           | (Snterm "EDIT" :: oprod) :: tl ->
             aux tl (edit_single_prod g oprod prods nt) add_nt
           | (Snterm "REPLACE" :: oprod) :: (Snterm "WITH" :: rprod) :: tl ->
+            report_undef_nts g rprod "";
             let prods' = (try
               let posn = find_first oprod prods nt in
               let prods = insert_after posn [rprod] prods in  (* insert new prod *)
@@ -985,10 +1101,12 @@ let apply_edit_file g edits =
           | (Snterm "REPLACE" :: _ as eprod) :: tl ->
             error "Missing WITH after '%s' in '%s'\n" (prod_to_str eprod) nt;
             aux tl prods add_nt
+          (* todo: check for unmatched editing keywords here *)
           | prod :: tl ->
             (* add a production *)
             if has_match prod prods then
               error "Duplicate production '%s' for %s\n" (prod_to_str prod) nt;
+            report_undef_nts g prod nt;
             aux tl (prods @ [prod]) add_nt
         in
         let prods, add_nt =
@@ -1001,25 +1119,6 @@ let apply_edit_file g edits =
 
 (*** main routines ***)
 
- (* get the nt's in the production, preserving order, don't worry about dups *)
- let nts_in_prod prod =
-  let rec traverse = function
-  | Sterm s -> []
-  | Snterm s -> [s]
-  | Slist1 sym
-  | Slist0 sym
-  | Sopt sym
-    -> traverse sym
-  | Slist1sep (sym, sep)
-  | Slist0sep (sym, sep)
-    -> traverse sym @ (traverse sep)
-  | Sparen sym_list -> List.concat (List.map traverse sym_list)
-  | Sprod sym_list_list -> List.concat (List.map (fun l -> List.concat (List.map traverse l)) sym_list_list)
-  | Sedit _
-  | Sedit2 _ -> []
-  in
-  List.rev (List.concat (List.map traverse prod))
-
   (* get the special tokens in the grammar *)
 let print_special_tokens g =
   let rec traverse set = function
@@ -1129,24 +1228,156 @@ let print_chunks g out fmt () =
 
     (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*)
     (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*)
+let index_of str list =
+  let rec index_of_r str list index =
+    match list with
+    | [] -> None
+    | hd :: list ->
+      if hd = str then Some index
+      else index_of_r str list (index+1)
+  in
+  index_of_r str list 0
 
-let start_symbols = ["vernac_toplevel"]
-(* don't report tokens as undefined *)
-let tokens = [ "bullet"; "field"; "ident"; "int"; "num"; "numeral"; "string" ]
+exception IsNone
 
-let report_bad_nts g file =
-  let rec get_nts refd defd bindings =
-    match bindings with
-    | [] -> refd, defd
-    | (nt, prods) :: tl ->
-      get_nts (List.fold_left (fun res prod ->
-                  StringSet.union res (StringSet.of_list (nts_in_prod prod)))
-                refd prods)
-        (StringSet.add nt defd) tl
+(* todo: raise exception for bad n? *)
+let rec nthcdr n list = if n <= 0 then list else nthcdr (n-1) (List.tl list)
+
+let pfx n list =
+  let rec pfx_r n res = function
+    | item :: tl -> if n < 0 then res else pfx_r (n-1) (item :: res) tl
+    | [] -> res
+  in
+  List.rev (pfx_r n [] list)
+
+(* todo: adjust Makefile to include Option.ml/mli *)
+let get_opt = function
+  | Some y -> y
+  | _ -> raise IsNone
+
+let get_range g start end_ =
+  let starti, endi = get_opt (index_of start !g.order), get_opt (index_of end_ !g.order) in
+  pfx (endi - starti) (nthcdr starti !g.order)
+
+let get_rangeset g start end_ = StringSet.of_list (get_range g start end_)
+
+let print_dominated g =
+  let info nt rangeset exclude =
+    let reachable = StringSet.of_list (nt_closure g nt exclude) in
+    let unreachable = StringSet.of_list (nt_closure g (List.hd start_symbols) (nt::exclude)) in
+    let dominated = StringSet.diff reachable unreachable in
+    Printf.printf "For %s, 'attribute' is: reachable = %b, unreachable = %b, dominated = %b\n" nt
+        (StringSet.mem "attribute" reachable)
+        (StringSet.mem "attribute" unreachable)
+        (StringSet.mem "attribute" dominated);
+    Printf.printf "  rangeset = %b excluded = %b\n"
+        (StringSet.mem "attribute" rangeset)
+        (List.mem "attribute" exclude);
+    reachable, dominated
+  in
+  let pr3 nt rangeset reachable dominated =
+    let missing = StringSet.diff dominated rangeset in
+    if not (StringSet.is_empty missing) then begin
+      Printf.printf "\nMissing in range for '%s':\n" nt;
+      StringSet.iter (fun nt -> Printf.printf "  %s\n" nt) missing
+    end;
+
+    let unneeded = StringSet.diff rangeset reachable in
+    if not (StringSet.is_empty unneeded) then begin
+      Printf.printf "\nUnneeded in range for '%s':\n" nt;
+      StringSet.iter (fun nt -> Printf.printf "  %s\n" nt) unneeded
+    end;
   in
-  let all_nts_ref, all_nts_def =
-    get_nts (StringSet.of_list tokens) (StringSet.of_list tokens) (NTMap.bindings !g.map) in
+  let pr2 nt rangeset exclude =
+    let reachable, dominated = info nt rangeset exclude in
+    pr3 nt rangeset reachable dominated
+  in
+  let pr nt end_ = pr2 nt (get_rangeset g nt end_) [] in
+
+  let ssr_ltac = ["ssr_first_else"; "ssrmmod"; "ssrdotac"; "ssrortacarg";
+      "ssrparentacarg"] in
+  let ssr_tac = ["ssrintrosarg"; "ssrhintarg"; "ssrtclarg"; "ssrseqarg"; "ssrmovearg";
+      "ssrrpat"; "ssrclauses"; "ssrcasearg"; "ssrarg"; "ssrapplyarg"; "ssrexactarg";
+      "ssrcongrarg"; "ssrterm"; "ssrrwargs"; "ssrunlockargs"; "ssrfixfwd"; "ssrcofixfwd";
+      "ssrfwdid"; "ssrposefwd"; "ssrsetfwd"; "ssrdgens"; "ssrhavefwdwbinders"; "ssrhpats_nobs";
+      "ssrhavefwd"; "ssrsufffwd"; "ssrwlogfwd"; "ssrhint"; "ssrclear"; "ssr_idcomma";
+      "ssrrwarg"; "ssrintros_ne"; "ssrhint3arg" ] @ ssr_ltac in
+  let ssr_cmd = ["ssr_modlocs"; "ssr_search_arg"; "ssrhintref"; "ssrhintref_list";
+      "ssrviewpos"; "ssrviewposspc"] in
+  let ltac = ["ltac_expr"; "ltac_expr0"; "ltac_expr1"; "ltac_expr2"; "ltac_expr3"] in
+  let term = ["term"; "term0"; "term1"; "term10"; "term100"; "term9";
+      "pattern"; "pattern0"; "pattern1"; "pattern10"] in
+
+  pr "term" "constr";
+
+  let ltac_rangeset = List.fold_left StringSet.union StringSet.empty
+                            [(get_rangeset g "ltac_expr" "tactic_atom");
+                            (get_rangeset g "toplevel_selector" "range_selector");
+                            (get_rangeset g "ltac_match_term" "match_pattern");
+                            (get_rangeset g "ltac_match_goal" "match_pattern_opt")] in
+  pr2 "ltac_expr" ltac_rangeset ("simple_tactic" :: ssr_tac);
+
+  let dec_vern_rangeset = get_rangeset g "decorated_vernac" "opt_coercion" in
+  let dev_vern_excl =
+      ["gallina_ext"; "command"; "tactic_mode"; "syntax"; "command_entry"] @ term @ ltac @ ssr_tac in
+  pr2 "decorated_vernac" dec_vern_rangeset dev_vern_excl;
+
+  let simp_tac_range = get_rangeset g "simple_tactic" "hypident_occ_list_comma" in
+  let simp_tac_excl = ltac @ ssr_tac in
+  pr2 "simple_tactic" simp_tac_range simp_tac_excl;
+
+  let cmd_range = get_rangeset g "command" "int_or_id_list_opt" in
+  let cmd_excl = ssr_tac @ ssr_cmd in
+  pr2 "command" cmd_range cmd_excl;
+
+  let syn_range = get_rangeset g "syntax" "constr_as_binder_kind" in
+  let syn_excl = ssr_tac @ ssr_cmd in
+  pr2 "syntax" syn_range syn_excl;
+
+  let gext_range = get_rangeset g "gallina_ext" "Structure_opt" in
+  let gext_excl = ssr_tac @ ssr_cmd in
+  pr2 "gallina_ext" gext_range gext_excl;
+
+  let qry_range = get_rangeset g "query_command" "searchabout_query_list" in
+  let qry_excl = ssr_tac @ ssr_cmd in
+  pr2 "query_command" qry_range qry_excl
+
+  (* todo: tactic_mode *)
+
+let check_range_consistency g start end_ =
+  let defined_list = get_range g start end_ in
+  let defined = StringSet.of_list defined_list in
+  let referenced = List.fold_left (fun set nt ->
+      let prods = NTMap.find nt !g.map in
+      let refs = List.concat (List.map nts_in_prod prods) in
+      StringSet.union set (StringSet.of_list refs))
+    StringSet.empty defined_list
+  in
+  let undef = StringSet.diff referenced defined in
+  let unused = StringSet.diff defined referenced in
+  if StringSet.cardinal unused > 0 || (StringSet.cardinal undef > 0) then begin
+    Printf.printf "\nFor range '%s' to '%s':\n  External reference:" start end_;
+    StringSet.iter (fun nt -> Printf.printf " %s" nt) undef;
+    Printf.printf "\n";
+    if StringSet.cardinal unused > 0 then begin
+      Printf.printf "  Unreferenced:";
+      StringSet.iter (fun nt -> Printf.printf " %s" nt) unused;
+      Printf.printf "\n"
+    end
+  end
+
+(* print info on symbols with a single production of a single nonterminal *)
+let check_singletons g =
+  NTMap.iter (fun nt prods ->
+      if List.length prods = 1 then
+        if List.length (remove_Sedit2 (List.hd prods)) = 1 then
+          warn "Singleton non-terminal, maybe SPLICE?: %s\n" nt
+        else
+          (*warn "Single production, maybe SPLICE?: %s\n" nt*) ())
+    !g.map
 
+let report_bad_nts g file =
+  let all_nts_ref, all_nts_def = get_refdef_nts g in
   let undef = StringSet.diff all_nts_ref all_nts_def in
   List.iter (fun nt -> warn "%s: Undefined symbol '%s'\n" file nt) (StringSet.elements undef);
 
@@ -1287,12 +1518,13 @@ let finish_with_file old_file verify =
   in
 
   let temp_file = (old_file ^ "_temp") in
-  if verify then
-    if (files_eq old_file temp_file || !exit_code <> 0) then
-      Sys.remove temp_file
-    else
-      error "%s is not current\n" old_file
-  else
+  if !exit_code <> 0 then
+    Sys.remove temp_file
+  else if verify then begin
+    if not (files_eq old_file temp_file) then
+      error "%s is not current\n" old_file;
+    Sys.remove temp_file
+  end else
     Sys.rename temp_file old_file
 
 let open_temp_bin file =
@@ -1342,21 +1574,13 @@ let process_rst g file args seen tac_prods cmd_prods =
   let ig_args_regex = Str.regexp "^[ \t]*\\([a-zA-Z0-9_\\.]*\\)[ \t]*\\([a-zA-Z0-9_\\.]*\\)" in
   let blank_regex = Str.regexp "^[ \t]*$" in
   let end_prodlist_regex = Str.regexp "^[ \t]*$" in
-  let rec index_of_r str list index =
-    match list with
-    | [] -> None
-    | hd :: list ->
-      if hd = str then Some index
-      else index_of_r str list (index+1)
-  in
-  let index_of str list = index_of_r str list 0 in
   let getline () =
     let line = input_line old_rst in
     incr linenum;
     line
   in
+  (* todo: maybe pass end_index? *)
   let output_insertgram start_index end_ indent is_coq_group =
-    let rec nthcdr n list = if n = 0 then list else nthcdr (n-1) (List.tl list) in
     let rec copy_prods list =
       match list with
       | [] -> ()
@@ -1390,10 +1614,12 @@ let process_rst g file args seen tac_prods cmd_prods =
         error "%s line %d: '%s' is undefined\n" file !linenum start;
       if end_index = None then
         error "%s line %d: '%s' is undefined\n" file !linenum end_;
+      if start_index <> None && end_index <> None then
+        check_range_consistency g start end_;
       match start_index, end_index with
       | Some start_index, Some end_index ->
         if start_index > end_index then
-          error "%s line %d: '%s' must appear before '%s' in .../orderedGrammar\n" file !linenum start end_
+          error "%s line %d: '%s' must appear before '%s' in orderedGrammar\n" file !linenum start end_
         else begin
           try
             let line2 = getline() in
@@ -1470,21 +1696,28 @@ let report_omitted_prods entries seen label split =
     end
   in
 
-  let first, last, n = List.fold_left (fun missing nt ->
-      let first, last, n = missing in
+  let first, last, n, total = List.fold_left (fun missing nt ->
+      let first, last, n, total = missing in
       if NTMap.mem nt seen then begin
         maybe_warn first last n;
-        "", "", 0
+        "", "", 0, total
       end else
-        (if first = "" then nt else first), nt, n + 1)
-    ("", "", 0) entries in
-  maybe_warn first last n
+        (if first = "" then nt else first), nt, n + 1, total + 1)
+    ("", "", 0, 0) entries in
+  maybe_warn first last n;
+  if total <> 0 then
+    Printf.eprintf "TOTAL %ss not included = %d\n" label total
 
 let process_grammar args =
   let symdef_map = ref StringMap.empty in
   let g = ref { map = NTMap.empty; order = [] } in
 
   let level_renames = read_mlg_files g args symdef_map in
+  if args.verbose then begin
+    Printf.printf "Keywords:\n";
+    StringSet.iter (fun kw -> Printf.printf "%s " kw) !keywords;
+    Printf.printf "\n\n";
+  end;
 
   (* rename nts with levels *)
   List.iter (fun b -> let (nt, prod) = b in
@@ -1546,6 +1779,8 @@ let process_grammar args =
       print_in_order out g `MLG !g.order StringSet.empty;
       close_out out;
       finish_with_file (dir "orderedGrammar") args.verify;
+      check_singletons g
+(*      print_dominated g*)
     end;
 
     if !exit_code = 0 then begin
@@ -1558,6 +1793,8 @@ let process_grammar args =
       let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; cmds=NTMap.empty } in
       List.iter (fun file -> process_rst g file args seen tac_prods cmd_prods) args.rst_files;
       report_omitted_prods !g.order !seen.nts "Nonterminal" "";
+      let out = open_out (dir "updated_rsts") in
+      close_out out;
       if args.check_tacs then
         report_omitted_prods tac_list !seen.tacs "Tactic" "\n                 ";
       if args.check_cmds then
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index a83638dd73..ebaeb392a5 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -73,12 +73,9 @@ operconstr200: [
 ]
 
 operconstr100: [
-| operconstr99 "<:" binder_constr
-| operconstr99 "<:" operconstr100
-| operconstr99 "<<:" binder_constr
-| operconstr99 "<<:" operconstr100
-| operconstr99 ":" binder_constr
-| operconstr99 ":" operconstr100
+| operconstr99 "<:" operconstr200
+| operconstr99 "<<:" operconstr200
+| operconstr99 ":" operconstr200
 | operconstr99 ":>"
 | operconstr99
 ]
@@ -126,26 +123,23 @@ operconstr0: [
 ]
 
 record_declaration: [
-| record_fields
+| record_fields_instance
 ]
 
-record_fields: [
-| record_field_declaration ";" record_fields
-| record_field_declaration
+record_fields_instance: [
+| record_field_instance ";" record_fields_instance
+| record_field_instance
 |
-| record_field ";" record_fields
-| record_field ";"
-| record_field
 ]
 
-record_field_declaration: [
+record_field_instance: [
 | global binders ":=" lconstr
 ]
 
 binder_constr: [
 | "forall" open_binders "," operconstr200
 | "fun" open_binders "=>" operconstr200
-| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200
+| "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
 | "let" single_fix "in" operconstr200
 | "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200
 | "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
@@ -153,11 +147,6 @@ binder_constr: [
 | "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
 | "if" operconstr200 return_type "then" operconstr200 "else" operconstr200
 | fix_constr
-| "if" operconstr200 "is" ssr_dthen ssr_else      (* ssr plugin *)
-| "if" operconstr200 "isn't" ssr_dthen ssr_else      (* ssr plugin *)
-| "let" ":" ssr_mpat ":=" lconstr "in" lconstr      (* ssr plugin *)
-| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr      (* ssr plugin *)
-| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr      (* ssr plugin *)
 ]
 
 appl_arg: [
@@ -213,7 +202,7 @@ fix_kw: [
 ]
 
 fix_decl: [
-| identref binders_fixannot type_cstr ":=" operconstr200
+| identref binders_fixannot let_type_cstr ":=" operconstr200
 ]
 
 match_constr: [
@@ -250,7 +239,6 @@ record_pattern: [
 
 record_patterns: [
 | record_pattern ";" record_patterns
-| record_pattern ";"
 | record_pattern
 |
 ]
@@ -260,8 +248,7 @@ pattern200: [
 ]
 
 pattern100: [
-| pattern99 ":" binder_constr
-| pattern99 ":" operconstr100
+| pattern99 ":" operconstr200
 | pattern99
 ]
 
@@ -306,8 +293,6 @@ fixannot: [
 | "{" "struct" identref "}"
 | "{" "wf" constr identref "}"
 | "{" "measure" constr OPT identref OPT constr "}"
-| "{" "struct" name "}"
-|
 ]
 
 impl_name_head: [
@@ -350,7 +335,6 @@ closed_binder: [
 | "`(" LIST1 typeclass_constraint SEP "," ")"
 | "`{" LIST1 typeclass_constraint SEP "," "}"
 | "'" pattern0
-| [ "of" | "&" ] operconstr99      (* ssr plugin *)
 ]
 
 typeclass_constraint: [
@@ -360,10 +344,8 @@ typeclass_constraint: [
 | operconstr200
 ]
 
-type_cstr: [
+let_type_cstr: [
 | OPT [ ":" lconstr ]
-| ":" lconstr
-|
 ]
 
 preident: [
@@ -467,14 +449,15 @@ bigint: [
 ]
 
 bar_cbrace: [
-| "|" "}"
+| test_nospace_pipe_closedcurly "|" "}"
 ]
 
 vernac_toplevel: [
 | "Drop" "."
 | "Quit" "."
-| "Backtrack" natural natural natural "."
+| "BackTo" natural "."
 | test_show_goal "Show" "Goal" natural "at" natural "."
+| "Show" "Proof" "Diffs" OPT "removed" "."
 | Pvernac.Vernac_.main_entry
 ]
 
@@ -560,7 +543,6 @@ command: [
 | "Reset" identref
 | "Back"
 | "Back" natural
-| "BackTo" natural
 | "Debug" "On"
 | "Debug" "Off"
 | "Declare" "Reduction" IDENT; ":=" red_expr
@@ -669,14 +651,27 @@ command: [
 | "Show" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
+| "Add" "InjTyp" constr      (* micromega plugin *)
+| "Add" "BinOp" constr      (* micromega plugin *)
+| "Add" "UnOp" constr      (* micromega plugin *)
+| "Add" "CstOp" constr      (* micromega plugin *)
+| "Add" "BinRel" constr      (* micromega plugin *)
+| "Add" "PropOp" constr      (* micromega plugin *)
+| "Add" "PropUOp" constr      (* micromega plugin *)
+| "Add" "Spec" constr      (* micromega plugin *)
+| "Add" "BinOpSpec" constr      (* micromega plugin *)
+| "Add" "UnOpSpec" constr      (* micromega plugin *)
+| "Add" "Saturate" constr      (* micromega plugin *)
+| "Show" "Zify" "InjTyp"      (* micromega plugin *)
+| "Show" "Zify" "BinOp"      (* micromega plugin *)
+| "Show" "Zify" "UnOp"      (* micromega plugin *)
+| "Show" "Zify" "CstOp"      (* micromega plugin *)
+| "Show" "Zify" "BinRel"      (* micromega plugin *)
+| "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" constr OPT ring_mods      (* setoid_ring plugin *)
 | "Print" "Rings"      (* setoid_ring plugin *)
 | "Add" "Field" ident ":" constr OPT field_mods      (* setoid_ring plugin *)
 | "Print" "Fields"      (* setoid_ring plugin *)
-| "Prenex" "Implicits" LIST1 global      (* ssr plugin *)
-| "Search" ssr_search_arg ssr_modlocs      (* ssr plugin *)
-| "Print" "Hint" "View" ssrviewpos      (* ssr plugin *)
-| "Hint" "View" ssrviewposspc LIST1 ssrhintref      (* ssr plugin *)
 | "Numeral" "Notation" reference reference reference ":" ident numnotoption
 | "String" "Notation" reference reference reference ":" ident
 ]
@@ -803,6 +798,7 @@ register_token: [
 
 register_type_token: [
 | "#int63_type"
+| "#float64_type"
 ]
 
 register_prim_token: [
@@ -830,6 +826,24 @@ register_prim_token: [
 | "#int63_lt"
 | "#int63_le"
 | "#int63_compare"
+| "#float64_opp"
+| "#float64_abs"
+| "#float64_eq"
+| "#float64_lt"
+| "#float64_le"
+| "#float64_compare"
+| "#float64_classify"
+| "#float64_add"
+| "#float64_sub"
+| "#float64_mul"
+| "#float64_div"
+| "#float64_sqrt"
+| "#float64_of_int63"
+| "#float64_normfr_mantissa"
+| "#float64_frshiftexp"
+| "#float64_ldshiftexp"
+| "#float64_next_up"
+| "#float64_next_down"
 ]
 
 thm_token: [
@@ -949,11 +963,16 @@ opt_coercion: [
 ]
 
 rec_definition: [
-| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
+| ident_decl binders_fixannot rec_type_cstr OPT [ ":=" lconstr ] decl_notation
 ]
 
 corec_definition: [
-| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
+| ident_decl binders rec_type_cstr OPT [ ":=" lconstr ] decl_notation
+]
+
+rec_type_cstr: [
+| ":" lconstr
+|
 ]
 
 scheme: [
@@ -973,6 +992,13 @@ record_field: [
 | LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notation
 ]
 
+record_fields: [
+| record_field ";" record_fields
+| record_field ";"
+| record_field
+|
+]
+
 record_binder_body: [
 | binders of_type_with_opt_coercion lconstr
 | binders of_type_with_opt_coercion lconstr ":=" lconstr
@@ -1048,7 +1074,6 @@ gallina_ext: [
 | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ]
 | "Export" "Set" option_table option_setting
 | "Export" "Unset" option_table
-| "Import" "Prenex" "Implicits"      (* ssr plugin *)
 ]
 
 export_token: [
@@ -1175,21 +1200,21 @@ arguments_modifier: [
 | "clear" "implicits" "and" "scopes"
 ]
 
-scope: [
+scope_delimiter: [
 | "%" IDENT
 ]
 
 argument_spec: [
-| OPT "!" name OPT scope
+| OPT "!" name OPT scope_delimiter
 ]
 
 argument_spec_block: [
 | argument_spec
 | "/"
 | "&"
-| "(" LIST1 argument_spec ")" OPT scope
-| "[" LIST1 argument_spec "]" OPT scope
-| "{" LIST1 argument_spec "}" OPT scope
+| "(" LIST1 argument_spec ")" OPT scope_delimiter
+| "[" LIST1 argument_spec "]" OPT scope_delimiter
+| "{" LIST1 argument_spec "}" OPT scope_delimiter
 ]
 
 more_implicits_block: [
@@ -1260,6 +1285,7 @@ printable: [
 | "Coercions"
 | "Coercion" "Paths" class_rawexpr class_rawexpr
 | "Canonical" "Projections"
+| "Typing" "Flags"
 | "Tables"
 | "Options"
 | "Hint"
@@ -1339,7 +1365,7 @@ positive_search_mark: [
 ]
 
 searchabout_query: [
-| positive_search_mark ne_string OPT scope
+| positive_search_mark ne_string OPT scope_delimiter
 | positive_search_mark constr_pattern
 ]
 
@@ -1725,6 +1751,9 @@ simple_tactic: [
 | "psatz_R" tactic      (* micromega plugin *)
 | "psatz_Q" int_or_var tactic      (* micromega plugin *)
 | "psatz_Q" tactic      (* micromega plugin *)
+| "iter_specs" tactic      (* micromega plugin *)
+| "zify_op"      (* micromega plugin *)
+| "saturate"      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
 | "omega" "with" LIST1 ident      (* omega plugin *)
@@ -1734,54 +1763,6 @@ simple_tactic: [
 | "protect_fv" string      (* setoid_ring plugin *)
 | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr      (* setoid_ring plugin *)
 | "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr      (* setoid_ring plugin *)
-| "YouShouldNotTypeThis" ssrintrosarg      (* ssr plugin *)
-| "by" ssrhintarg      (* ssr plugin *)
-| "YouShouldNotTypeThis" "do" ssrdoarg      (* ssr plugin *)
-| "YouShouldNotTypeThis" ssrtclarg ssrseqdir ssrseqarg      (* ssr plugin *)
-| "clear" natural      (* ssr plugin *)
-| "move" ssrmovearg ssrrpat      (* ssr plugin *)
-| "move" ssrmovearg ssrclauses      (* ssr plugin *)
-| "move" ssrrpat      (* ssr plugin *)
-| "move"      (* ssr plugin *)
-| "case" ssrcasearg ssrclauses      (* ssr plugin *)
-| "case"      (* ssr plugin *)
-| "elim" ssrarg ssrclauses      (* ssr plugin *)
-| "elim"      (* ssr plugin *)
-| "apply" ssrapplyarg      (* ssr plugin *)
-| "apply"      (* ssr plugin *)
-| "exact" ssrexactarg      (* ssr plugin *)
-| "exact"      (* ssr plugin *)
-| "exact" "<:" lconstr      (* ssr plugin *)
-| "congr" ssrcongrarg      (* ssr plugin *)
-| "ssrinstancesofruleL2R" ssrterm      (* ssr plugin *)
-| "ssrinstancesofruleR2L" ssrterm      (* ssr plugin *)
-| "rewrite" ssrrwargs ssrclauses      (* ssr plugin *)
-| "unlock" ssrunlockargs ssrclauses      (* ssr plugin *)
-| "pose" ssrfixfwd      (* ssr plugin *)
-| "pose" ssrcofixfwd      (* ssr plugin *)
-| "pose" ssrfwdid ssrposefwd      (* ssr plugin *)
-| "set" ssrfwdid ssrsetfwd ssrclauses      (* ssr plugin *)
-| "abstract" ssrdgens      (* ssr plugin *)
-| "have" ssrhavefwdwbinders      (* ssr plugin *)
-| "have" "suff" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
-| "have" "suffices" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
-| "suff" "have" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
-| "suffices" "have" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
-| "suff" ssrsufffwd      (* ssr plugin *)
-| "suffices" ssrsufffwd      (* ssr plugin *)
-| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "under" ssrrwarg      (* ssr plugin *)
-| "under" ssrrwarg ssrintros_ne      (* ssr plugin *)
-| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg      (* ssr plugin *)
-| "under" ssrrwarg "do" ssrhint3arg      (* ssr plugin *)
-| "ssrinstancesoftpat" cpattern      (* ssrmatching plugin *)
 ]
 
 mlname: [
@@ -1891,10 +1872,6 @@ test_lpar_id_colon: [
 | local_test_lpar_id_colon
 ]
 
-orient_string: [
-| orient preident
-]
-
 comparison: [
 | "="
 | "<"
@@ -1977,9 +1954,6 @@ tactic_expr4: [
 | tactic_expr3 ";" tactic_expr3
 | tactic_expr3 ";" tactic_then_locality tactic_then_gen "]"
 | tactic_expr3
-| tactic_expr5 ";" "first" ssr_first_else      (* ssr plugin *)
-| tactic_expr5 ";" "first" ssrseqarg      (* ssr plugin *)
-| tactic_expr5 ";" "last" ssrseqarg      (* ssr plugin *)
 ]
 
 tactic_expr3: [
@@ -1996,10 +1970,6 @@ tactic_expr3: [
 | "abstract" tactic_expr2 "using" ident
 | selector tactic_expr3
 | tactic_expr2
-| "do" ssrmmod ssrdotac ssrclauses      (* ssr plugin *)
-| "do" ssrortacarg ssrclauses      (* ssr plugin *)
-| "do" int_or_var ssrmmod ssrdotac ssrclauses      (* ssr plugin *)
-| "abstract" ssrdgens      (* ssr plugin *)
 ]
 
 tactic_expr2: [
@@ -2023,14 +1993,12 @@ tactic_expr1: [
 | tactic_arg
 | reference LIST0 tactic_arg_compat
 | tactic_expr0
-| tactic_expr5 ssrintros_ne      (* ssr plugin *)
 ]
 
 tactic_expr0: [
 | "(" tactic_expr5 ")"
 | "[" ">" tactic_then_gen "]"
 | tactic_atom
-| ssrparentacarg      (* ssr plugin *)
 ]
 
 failkw: [
@@ -2422,8 +2390,6 @@ hypident: [
 | id_or_meta
 | "(" "type" "of" id_or_meta ")"
 | "(" "value" "of" id_or_meta ")"
-| "(" "type" "of" Prim.identref ")"      (* ssr plugin *)
-| "(" "value" "of" Prim.identref ")"      (* ssr plugin *)
 ]
 
 hypident_occ: [
@@ -2462,13 +2428,24 @@ in_hyp_as: [
 |
 ]
 
+orient_rw: [
+| "->"
+| "<-"
+|
+]
+
 simple_binder: [
 | name
 | "(" LIST1 name ":" lconstr ")"
 ]
 
 fixdecl: [
-| "(" ident LIST0 simple_binder fixannot ":" lconstr ")"
+| "(" ident LIST0 simple_binder struct_annot ":" lconstr ")"
+]
+
+struct_annot: [
+| "{" "struct" name "}"
+|
 ]
 
 cofixdecl: [
@@ -2525,7 +2502,7 @@ rewriter: [
 ]
 
 oriented_rewriter: [
-| orient rewriter
+| orient_rw rewriter
 ]
 
 induction_clause: [
@@ -2564,608 +2541,6 @@ field_mods: [
 | "(" LIST1 field_mod SEP "," ")"      (* setoid_ring plugin *)
 ]
 
-ssrtacarg: [
-| tactic_expr5      (* ssr plugin *)
-]
-
-ssrtac3arg: [
-| tactic_expr3      (* ssr plugin *)
-]
-
-ssrtclarg: [
-| ssrtacarg      (* ssr plugin *)
-]
-
-ssrhyp: [
-| ident      (* ssr plugin *)
-]
-
-ssrhoi_hyp: [
-| ident      (* ssr plugin *)
-]
-
-ssrhoi_id: [
-| ident      (* ssr plugin *)
-]
-
-ssrsimpl_ne: [
-| "//="      (* ssr plugin *)
-| "/="      (* ssr plugin *)
-| test_ssrslashnum11 "/" natural "/" natural "="      (* ssr plugin *)
-| test_ssrslashnum10 "/" natural "/"      (* ssr plugin *)
-| test_ssrslashnum10 "/" natural "="      (* ssr plugin *)
-| test_ssrslashnum10 "/" natural "/="      (* ssr plugin *)
-| test_ssrslashnum10 "/" natural "/" "="      (* ssr plugin *)
-| test_ssrslashnum01 "//" natural "="      (* ssr plugin *)
-| test_ssrslashnum00 "//"      (* ssr plugin *)
-]
-
-ssrclear_ne: [
-| "{" LIST1 ssrhyp "}"      (* ssr plugin *)
-]
-
-ssrclear: [
-| ssrclear_ne      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrindex: [
-| int_or_var      (* ssr plugin *)
-]
-
-ssrocc: [
-| natural LIST0 natural      (* ssr plugin *)
-| "-" LIST0 natural      (* ssr plugin *)
-| "+" LIST0 natural      (* ssr plugin *)
-]
-
-ssrmmod: [
-| "!"      (* ssr plugin *)
-| LEFTQMARK      (* ssr plugin *)
-| "?"      (* ssr plugin *)
-]
-
-ssrmult_ne: [
-| natural ssrmmod      (* ssr plugin *)
-| ssrmmod      (* ssr plugin *)
-]
-
-ssrmult: [
-| ssrmult_ne      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrdocc: [
-| "{" ssrocc "}"      (* ssr plugin *)
-| "{" LIST0 ssrhyp "}"      (* ssr plugin *)
-]
-
-ssrterm: [
-| "YouShouldNotTypeThis" constr      (* ssr plugin *)
-| ssrtermkind Pcoq.Constr.constr      (* ssr plugin *)
-]
-
-ast_closure_term: [
-| term_annotation constr      (* ssr plugin *)
-]
-
-ast_closure_lterm: [
-| term_annotation lconstr      (* ssr plugin *)
-]
-
-ssrbwdview: [
-| "YouShouldNotTypeThis"      (* ssr plugin *)
-| test_not_ssrslashnum "/" Pcoq.Constr.constr      (* ssr plugin *)
-| test_not_ssrslashnum "/" Pcoq.Constr.constr ssrbwdview      (* ssr plugin *)
-]
-
-ssrfwdview: [
-| "YouShouldNotTypeThis"      (* ssr plugin *)
-| test_not_ssrslashnum "/" ast_closure_term      (* ssr plugin *)
-| test_not_ssrslashnum "/" ast_closure_term ssrfwdview      (* ssr plugin *)
-]
-
-ident_no_do: [
-| "YouShouldNotTypeThis" ident      (* ssr plugin *)
-| test_ident_no_do IDENT      (* ssr plugin *)
-]
-
-ssripat: [
-| "_"      (* ssr plugin *)
-| "*"      (* ssr plugin *)
-| ">"      (* ssr plugin *)
-| ident_no_do      (* ssr plugin *)
-| "?"      (* ssr plugin *)
-| "+"      (* ssr plugin *)
-| "++"      (* ssr plugin *)
-| ssrsimpl_ne      (* ssr plugin *)
-| ssrdocc "->"      (* ssr plugin *)
-| ssrdocc "<-"      (* ssr plugin *)
-| ssrdocc      (* ssr plugin *)
-| "->"      (* ssr plugin *)
-| "<-"      (* ssr plugin *)
-| "-"      (* ssr plugin *)
-| "-/" "="      (* ssr plugin *)
-| "-/="      (* ssr plugin *)
-| "-/" "/"      (* ssr plugin *)
-| "-//"      (* ssr plugin *)
-| "-/" integer "/"      (* ssr plugin *)
-| "-/" "/="      (* ssr plugin *)
-| "-//" "="      (* ssr plugin *)
-| "-//="      (* ssr plugin *)
-| "-/" integer "/="      (* ssr plugin *)
-| "-/" integer "/" integer "="      (* ssr plugin *)
-| ssrfwdview      (* ssr plugin *)
-| "[" ":" LIST0 ident "]"      (* ssr plugin *)
-| "[:" LIST0 ident "]"      (* ssr plugin *)
-| ssrcpat      (* ssr plugin *)
-]
-
-ssripats: [
-| ssripat ssripats      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssriorpat: [
-| ssripats "|" ssriorpat      (* ssr plugin *)
-| ssripats "|-" ">" ssriorpat      (* ssr plugin *)
-| ssripats "|-" ssriorpat      (* ssr plugin *)
-| ssripats "|->" ssriorpat      (* ssr plugin *)
-| ssripats "||" ssriorpat      (* ssr plugin *)
-| ssripats "|||" ssriorpat      (* ssr plugin *)
-| ssripats "||||" ssriorpat      (* ssr plugin *)
-| ssripats      (* ssr plugin *)
-]
-
-ssrcpat: [
-| "YouShouldNotTypeThis" ssriorpat      (* ssr plugin *)
-| test_nohidden "[" hat "]"      (* ssr plugin *)
-| test_nohidden "[" ssriorpat "]"      (* ssr plugin *)
-| test_nohidden "[=" ssriorpat "]"      (* ssr plugin *)
-]
-
-hat: [
-| "^" ident      (* ssr plugin *)
-| "^" "~" ident      (* ssr plugin *)
-| "^" "~" natural      (* ssr plugin *)
-| "^~" ident      (* ssr plugin *)
-| "^~" natural      (* ssr plugin *)
-]
-
-ssripats_ne: [
-| ssripat ssripats      (* ssr plugin *)
-]
-
-ssrhpats: [
-| ssripats      (* ssr plugin *)
-]
-
-ssrhpats_wtransp: [
-| ssripats      (* ssr plugin *)
-| ssripats "@" ssripats      (* ssr plugin *)
-]
-
-ssrhpats_nobs: [
-| ssripats      (* ssr plugin *)
-]
-
-ssrrpat: [
-| "->"      (* ssr plugin *)
-| "<-"      (* ssr plugin *)
-]
-
-ssrintros_ne: [
-| "=>" ssripats_ne      (* ssr plugin *)
-]
-
-ssrintros: [
-| ssrintros_ne      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrintrosarg: [
-| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne      (* ssr plugin *)
-]
-
-ssrfwdid: [
-| test_ssrfwdid Prim.ident      (* ssr plugin *)
-]
-
-ssrortacs: [
-| ssrtacarg "|" ssrortacs      (* ssr plugin *)
-| ssrtacarg "|"      (* ssr plugin *)
-| ssrtacarg      (* ssr plugin *)
-| "|" ssrortacs      (* ssr plugin *)
-| "|"      (* ssr plugin *)
-]
-
-ssrhintarg: [
-| "[" "]"      (* ssr plugin *)
-| "[" ssrortacs "]"      (* ssr plugin *)
-| ssrtacarg      (* ssr plugin *)
-]
-
-ssrhint3arg: [
-| "[" "]"      (* ssr plugin *)
-| "[" ssrortacs "]"      (* ssr plugin *)
-| ssrtac3arg      (* ssr plugin *)
-]
-
-ssrortacarg: [
-| "[" ssrortacs "]"      (* ssr plugin *)
-]
-
-ssrhint: [
-|      (* ssr plugin *)
-| "by" ssrhintarg      (* ssr plugin *)
-]
-
-ssrwgen: [
-| ssrclear_ne      (* ssr plugin *)
-| ssrhoi_hyp      (* ssr plugin *)
-| "@" ssrhoi_hyp      (* ssr plugin *)
-| "(" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
-| "(" ssrhoi_id ")"      (* ssr plugin *)
-| "(@" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
-| "(" "@" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
-]
-
-ssrclausehyps: [
-| ssrwgen "," ssrclausehyps      (* ssr plugin *)
-| ssrwgen ssrclausehyps      (* ssr plugin *)
-| ssrwgen      (* ssr plugin *)
-]
-
-ssrclauses: [
-| "in" ssrclausehyps "|-" "*"      (* ssr plugin *)
-| "in" ssrclausehyps "|-"      (* ssr plugin *)
-| "in" ssrclausehyps "*"      (* ssr plugin *)
-| "in" ssrclausehyps      (* ssr plugin *)
-| "in" "|-" "*"      (* ssr plugin *)
-| "in" "*"      (* ssr plugin *)
-| "in" "*" "|-"      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrfwd: [
-| ":=" ast_closure_lterm      (* ssr plugin *)
-| ":" ast_closure_lterm ":=" ast_closure_lterm      (* ssr plugin *)
-]
-
-ssrbvar: [
-| ident      (* ssr plugin *)
-| "_"      (* ssr plugin *)
-]
-
-ssrbinder: [
-| ssrbvar      (* ssr plugin *)
-| "(" ssrbvar ")"      (* ssr plugin *)
-| "(" ssrbvar ":" lconstr ")"      (* ssr plugin *)
-| "(" ssrbvar LIST1 ssrbvar ":" lconstr ")"      (* ssr plugin *)
-| "(" ssrbvar ":" lconstr ":=" lconstr ")"      (* ssr plugin *)
-| "(" ssrbvar ":=" lconstr ")"      (* ssr plugin *)
-| [ "of" | "&" ] operconstr99      (* ssr plugin *)
-]
-
-ssrstruct: [
-| "{" "struct" ident "}"      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrposefwd: [
-| LIST0 ssrbinder ssrfwd      (* ssr plugin *)
-]
-
-ssrfixfwd: [
-| "fix" ssrbvar LIST0 ssrbinder ssrstruct ssrfwd      (* ssr plugin *)
-]
-
-ssrcofixfwd: [
-| "cofix" ssrbvar LIST0 ssrbinder ssrfwd      (* ssr plugin *)
-]
-
-ssrsetfwd: [
-| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern      (* ssr plugin *)
-| ":" ast_closure_lterm ":=" lcpattern      (* ssr plugin *)
-| ":=" "{" ssrocc "}" cpattern      (* ssr plugin *)
-| ":=" lcpattern      (* ssr plugin *)
-]
-
-ssrhavefwd: [
-| ":" ast_closure_lterm ssrhint      (* ssr plugin *)
-| ":" ast_closure_lterm ":=" ast_closure_lterm      (* ssr plugin *)
-| ":" ast_closure_lterm ":="      (* ssr plugin *)
-| ":=" ast_closure_lterm      (* ssr plugin *)
-]
-
-ssrhavefwdwbinders: [
-| ssrhpats_wtransp LIST0 ssrbinder ssrhavefwd      (* ssr plugin *)
-]
-
-ssrdoarg: [
-]
-
-ssrseqarg: [
-| ssrswap      (* ssr plugin *)
-| ssrseqidx ssrortacarg OPT ssrorelse      (* ssr plugin *)
-| ssrseqidx ssrswap      (* ssr plugin *)
-| tactic_expr3      (* ssr plugin *)
-]
-
-ssrseqidx: [
-| test_ssrseqvar Prim.ident      (* ssr plugin *)
-| Prim.natural      (* ssr plugin *)
-]
-
-ssrswap: [
-| "first"      (* ssr plugin *)
-| "last"      (* ssr plugin *)
-]
-
-ssrorelse: [
-| "||" tactic_expr2      (* ssr plugin *)
-]
-
-Prim.ident: [
-| IDENT ssr_null_entry      (* ssr plugin *)
-]
-
-ssrparentacarg: [
-| "(" tactic_expr5 ")"      (* ssr plugin *)
-]
-
-ssrdotac: [
-| tactic_expr3      (* ssr plugin *)
-| ssrortacarg      (* ssr plugin *)
-]
-
-ssrseqdir: [
-]
-
-ssr_first: [
-| ssr_first ssrintros_ne      (* ssr plugin *)
-| "[" LIST0 tactic_expr5 SEP "|" "]"      (* ssr plugin *)
-]
-
-ssr_first_else: [
-| ssr_first ssrorelse      (* ssr plugin *)
-| ssr_first      (* ssr plugin *)
-]
-
-ssrgen: [
-| ssrdocc cpattern      (* ssr plugin *)
-| cpattern      (* ssr plugin *)
-]
-
-ssrdgens_tl: [
-| "{" LIST1 ssrhyp "}" cpattern ssrdgens_tl      (* ssr plugin *)
-| "{" LIST1 ssrhyp "}"      (* ssr plugin *)
-| "{" ssrocc "}" cpattern ssrdgens_tl      (* ssr plugin *)
-| "/" ssrdgens_tl      (* ssr plugin *)
-| cpattern ssrdgens_tl      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrdgens: [
-| ":" ssrgen ssrdgens_tl      (* ssr plugin *)
-]
-
-ssreqid: [
-| test_ssreqid ssreqpat      (* ssr plugin *)
-| test_ssreqid      (* ssr plugin *)
-]
-
-ssreqpat: [
-| Prim.ident      (* ssr plugin *)
-| "_"      (* ssr plugin *)
-| "?"      (* ssr plugin *)
-| "+"      (* ssr plugin *)
-| ssrdocc "->"      (* ssr plugin *)
-| ssrdocc "<-"      (* ssr plugin *)
-| "->"      (* ssr plugin *)
-| "<-"      (* ssr plugin *)
-]
-
-ssrarg: [
-| ssrfwdview ssreqid ssrdgens ssrintros      (* ssr plugin *)
-| ssrfwdview ssrclear ssrintros      (* ssr plugin *)
-| ssreqid ssrdgens ssrintros      (* ssr plugin *)
-| ssrclear_ne ssrintros      (* ssr plugin *)
-| ssrintros_ne      (* ssr plugin *)
-]
-
-ssrmovearg: [
-| ssrarg      (* ssr plugin *)
-]
-
-ssrcasearg: [
-| ssrarg      (* ssr plugin *)
-]
-
-ssragen: [
-| "{" LIST1 ssrhyp "}" ssrterm      (* ssr plugin *)
-| ssrterm      (* ssr plugin *)
-]
-
-ssragens: [
-| "{" LIST1 ssrhyp "}" ssrterm ssragens      (* ssr plugin *)
-| "{" LIST1 ssrhyp "}"      (* ssr plugin *)
-| ssrterm ssragens      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrapplyarg: [
-| ":" ssragen ssragens ssrintros      (* ssr plugin *)
-| ssrclear_ne ssrintros      (* ssr plugin *)
-| ssrintros_ne      (* ssr plugin *)
-| ssrbwdview ":" ssragen ssragens ssrintros      (* ssr plugin *)
-| ssrbwdview ssrclear ssrintros      (* ssr plugin *)
-]
-
-ssrexactarg: [
-| ":" ssragen ssragens      (* ssr plugin *)
-| ssrbwdview ssrclear      (* ssr plugin *)
-| ssrclear_ne      (* ssr plugin *)
-]
-
-ssrcongrarg: [
-| natural constr ssrdgens      (* ssr plugin *)
-| natural constr      (* ssr plugin *)
-| constr ssrdgens      (* ssr plugin *)
-| constr      (* ssr plugin *)
-]
-
-ssrrwocc: [
-| "{" LIST0 ssrhyp "}"      (* ssr plugin *)
-| "{" ssrocc "}"      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrrule_ne: [
-| test_not_ssrslashnum [ "/" ssrterm | ssrterm | ssrsimpl_ne ]      (* ssr plugin *)
-| ssrsimpl_ne      (* ssr plugin *)
-]
-
-ssrrule: [
-| ssrrule_ne      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrpattern_squarep: [
-| "[" rpattern "]"      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrpattern_ne_squarep: [
-| "[" rpattern "]"      (* ssr plugin *)
-]
-
-ssrrwarg: [
-| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
-| "-/" ssrterm      (* ssr plugin *)
-| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
-| "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne      (* ssr plugin *)
-| "{" LIST1 ssrhyp "}" ssrrule      (* ssr plugin *)
-| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
-| "{" "}" ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
-| ssrpattern_ne_squarep ssrrule_ne      (* ssr plugin *)
-| ssrrule_ne      (* ssr plugin *)
-]
-
-ssrrwargs: [
-| test_ssr_rw_syntax LIST1 ssrrwarg      (* ssr plugin *)
-]
-
-ssrunlockarg: [
-| "{" ssrocc "}" ssrterm      (* ssr plugin *)
-| ssrterm      (* ssr plugin *)
-]
-
-ssrunlockargs: [
-| LIST0 ssrunlockarg      (* ssr plugin *)
-]
-
-ssrsufffwd: [
-| ssrhpats LIST0 ssrbinder ":" ast_closure_lterm ssrhint      (* ssr plugin *)
-]
-
-ssrwlogfwd: [
-| ":" LIST0 ssrwgen "/" ast_closure_lterm      (* ssr plugin *)
-]
-
-ssr_idcomma: [
-|      (* ssr plugin *)
-| test_idcomma [ IDENT | "_" ] ","      (* ssr plugin *)
-]
-
-ssr_rtype: [
-| "return" operconstr100      (* ssr plugin *)
-]
-
-ssr_mpat: [
-| pattern200      (* ssr plugin *)
-]
-
-ssr_dpat: [
-| ssr_mpat "in" pattern200 ssr_rtype      (* ssr plugin *)
-| ssr_mpat ssr_rtype      (* ssr plugin *)
-| ssr_mpat      (* ssr plugin *)
-]
-
-ssr_dthen: [
-| ssr_dpat "then" lconstr      (* ssr plugin *)
-]
-
-ssr_elsepat: [
-| "else"      (* ssr plugin *)
-]
-
-ssr_else: [
-| ssr_elsepat lconstr      (* ssr plugin *)
-]
-
-ssr_search_item: [
-| string      (* ssr plugin *)
-| string "%" preident      (* ssr plugin *)
-| constr_pattern      (* ssr plugin *)
-]
-
-ssr_search_arg: [
-| "-" ssr_search_item ssr_search_arg      (* ssr plugin *)
-| ssr_search_item ssr_search_arg      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssr_modlocs: [
-|      (* ssr plugin *)
-| "in" LIST1 modloc      (* ssr plugin *)
-]
-
-modloc: [
-| "-" global      (* ssr plugin *)
-| global      (* ssr plugin *)
-]
-
-ssrhintref: [
-| constr      (* ssr plugin *)
-| constr "|" natural      (* ssr plugin *)
-]
-
-ssrviewpos: [
-| "for" "move" "/"      (* ssr plugin *)
-| "for" "apply" "/"      (* ssr plugin *)
-| "for" "apply" "/" "/"      (* ssr plugin *)
-| "for" "apply" "//"      (* ssr plugin *)
-|      (* ssr plugin *)
-]
-
-ssrviewposspc: [
-| ssrviewpos      (* ssr plugin *)
-]
-
-rpattern: [
-| lconstr      (* ssrmatching plugin *)
-| "in" lconstr      (* ssrmatching plugin *)
-| lconstr "in" lconstr      (* ssrmatching plugin *)
-| "in" lconstr "in" lconstr      (* ssrmatching plugin *)
-| lconstr "in" lconstr "in" lconstr      (* ssrmatching plugin *)
-| lconstr "as" lconstr "in" lconstr      (* ssrmatching plugin *)
-]
-
-cpattern: [
-| "Qed" constr      (* ssrmatching plugin *)
-| ssrtermkind constr      (* ssrmatching plugin *)
-]
-
-lcpattern: [
-| "Qed" lconstr      (* ssrmatching plugin *)
-| ssrtermkind lconstr      (* ssrmatching plugin *)
-]
-
-ssrpatternarg: [
-| rpattern      (* ssrmatching plugin *)
-]
-
 numnotoption: [
 |
 | "(" "warning" "after" bigint ")"
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index cd6e11505c..545ccde03a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -3,603 +3,541 @@ doc_grammar will modify this file to add/remove nonterminals and productions
 to match editedGrammar, which will remove comments.  Not compiled into Coq *)
 DOC_GRAMMAR
 
-global: [
-| reference
-]
-
-constr_pattern: [
-| term
-]
-
-sort: [
-| "Set"
-| "Prop"
-| "SProp"
-| "Type"
-| "Type" "@{" "_" "}"
-| "Type" "@{" universe "}"
-]
-
-sort_family: [
-| "Set"
-| "Prop"
-| "SProp"
-| "Type"
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "BackTo" num "."
+| "Show" "Goal" num "at" num "."
+| "Show" "Proof" "Diffs" removed_opt "."
+| vernac_control
 ]
 
-universe_increment: [
-| "+" natural
+removed_opt: [
+| "removed"
 | empty
 ]
 
-universe_name: [
-| global
-| "Set"
-| "Prop"
+tactic_mode: [
+| toplevel_selector_opt query_command
+| toplevel_selector_opt "{"
+| toplevel_selector_opt ltac_info_opt ltac_expr ltac_use_default
+| "par" ":" ltac_info_opt ltac_expr ltac_use_default
 ]
 
-universe_expr: [
-| universe_name universe_increment
+toplevel_selector_opt: [
+| toplevel_selector
+| empty
 ]
 
-universe: [
-| "max" "(" universe_expr_list_comma ")"
-| universe_expr
+ltac_info_opt: [
+| "Info" num
+| empty
 ]
 
-universe_expr_list_comma: [
-| universe_expr_list_comma "," universe_expr
-| universe_expr
+ltac_use_default: [
+| "."
+| "..."
 ]
 
-lconstr: [
-| operconstr200
-| lconstr
+vernac_control: [
+| "Time" vernac_control
+| "Redirect" string vernac_control
+| "Timeout" num vernac_control
+| "Fail" vernac_control
+| quoted_attributes_list_opt vernac
 ]
 
 term: [
-| operconstr8
-| "@" global instance
+| "forall" open_binders "," term
+| "fun" open_binders "=>" term
+| term_let
+| "if" term as_return_type_opt "then" term "else" term
+| term_fix
+| term100
 ]
 
-operconstr200: [
-| binder_constr
-| operconstr100
+term100: [
+| term_cast
+| term10
 ]
 
-operconstr100: [
-| operconstr99 "<:" binder_constr
-| operconstr99 "<:" operconstr100
-| operconstr99 "<<:" binder_constr
-| operconstr99 "<<:" operconstr100
-| operconstr99 ":" binder_constr
-| operconstr99 ":" operconstr100
-| operconstr99 ":>"
-| operconstr99
+term10: [
+| term1 args
+| "@" qualid universe_annot_opt term1_list_opt
+| term1
 ]
 
-operconstr99: [
-| operconstr90
+args: [
+| args arg
+| arg
 ]
 
-operconstr90: [
-| operconstr10
+arg: [
+| "(" ident ":=" term ")"
+| term1
 ]
 
-operconstr10: [
-| operconstr9 appl_arg_list
-| "@" global instance operconstr9_list_opt
-| "@" pattern_identref ident_list
-| operconstr9
-]
-
-appl_arg_list: [
-| appl_arg_list appl_arg
-| appl_arg
-]
-
-operconstr9: [
-| ".." operconstr0 ".."
-| operconstr8
-]
-
-operconstr8: [
-| operconstr1
+term1_list_opt: [
+| term1_list_opt term1
+| empty
 ]
 
-operconstr1: [
-| operconstr0 ".(" global appl_arg_list_opt ")"
-| operconstr0 ".(" "@" global operconstr9_list_opt ")"
-| operconstr0 "%" IDENT
-| operconstr0
+empty: [
+|
 ]
 
-appl_arg_list_opt: [
-| appl_arg_list_opt appl_arg
-| empty
+term1: [
+| term_projection
+| term0 "%" ident
+| term0
 ]
 
-operconstr9_list_opt: [
-| operconstr9_list_opt operconstr9
+args_opt: [
+| args
 | empty
 ]
 
-operconstr0: [
-| atomic_constr
-| match_constr
-| "(" operconstr200 ")"
-| "{|" record_declaration bar_cbrace
-| "{" binder_constr "}"
-| "`{" operconstr200 "}"
-| "`(" operconstr200 ")"
+term0: [
+| qualid universe_annot_opt
+| sort
+| numeral
+| string
+| "_"
+| term_evar
+| term_match
+| "(" term ")"
+| "{|" fields_def "|}"
+| "`{" term "}"
+| "`(" term ")"
 | "ltac" ":" "(" ltac_expr ")"
 ]
 
-record_declaration: [
-| record_fields
-]
-
-record_fields: [
-| record_field_declaration ";" record_fields
-| record_field_declaration
+fields_def: [
+| field_def ";" fields_def
+| field_def
 | empty
-| record_field ";" record_fields
-| record_field ";"
-| record_field
-]
-
-record_field_declaration: [
-| global binders ":=" lconstr
 ]
 
-binder_constr: [
-| "forall" open_binders "," operconstr200
-| "fun" open_binders "=>" operconstr200
-| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200
-| "let" single_fix "in" operconstr200
-| "let" name_alt return_type ":=" operconstr200 "in" operconstr200
-| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
-| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
-| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
-| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200
-| fix_constr
-| "if" operconstr200 "is" ssr_dthen ssr_else      (* ssr plugin *)
-| "if" operconstr200 "isn't" ssr_dthen ssr_else      (* ssr plugin *)
-| "let" ":" ssr_mpat ":=" lconstr "in" lconstr      (* ssr plugin *)
-| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr      (* ssr plugin *)
-| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr      (* ssr plugin *)
+field_def: [
+| qualid binders_opt ":=" term
 ]
 
-name_alt: [
-| "(" name_list_comma_opt ")"
-| "()"
+binders_opt: [
+| binders
+| empty
 ]
 
-name_list_comma_opt: [
-| name_list_comma
-| empty
+term_projection: [
+| term0 ".(" qualid args_opt ")"
+| term0 ".(" "@" qualid term1_list_opt ")"
 ]
 
-name_list_comma: [
-| name_list_comma "," name
-| name
+term_evar: [
+| "?[" ident "]"
+| "?[" "?" ident "]"
+| "?" ident evar_bindings_opt
 ]
 
-name_list_opt: [
-| name_list_opt name
+evar_bindings_opt: [
+| "@{" evar_bindings_semi "}"
 | empty
 ]
 
-name_list: [
-| name_list name
-| name
+evar_bindings_semi: [
+| evar_bindings_semi ";" evar_binding
+| evar_binding
 ]
 
-appl_arg: [
-| lpar_id_coloneq lconstr ")"
-| operconstr9
+evar_binding: [
+| ident ":=" term
 ]
 
-atomic_constr: [
-| global instance
-| sort
-| NUMERAL
-| string
-| "_"
-| "?" "[" ident "]"
-| "?" "[" "?" ident "]"
-| "?" ident evar_instance
+dangling_pattern_extension_rule: [
+| "@" "?" ident ident_list
 ]
 
-inst: [
-| ident ":=" lconstr
+ident_list: [
+| ident_list ident
+| ident
 ]
 
-evar_instance: [
-| "@{" inst_list_semi "}"
+record_fields: [
+| record_field ";" record_fields
+| record_field ";"
+| record_field
 | empty
 ]
 
-inst_list_semi: [
-| inst_list_semi ";" inst
-| inst
-]
-
-instance: [
-| "@{" universe_level_list_opt "}"
-| empty
+record_field: [
+| quoted_attributes_list_opt record_binder num_opt2 decl_notation
 ]
 
-universe_level_list_opt: [
-| universe_level_list_opt universe_level
+decl_notation: [
+| "where" one_decl_notation_list
 | empty
 ]
 
-universe_level: [
-| "Set"
-| "Prop"
-| "Type"
-| "_"
-| global
-]
-
-fix_constr: [
-| single_fix
-| single_fix "with" fix_decl_list "for" ident
-]
-
-fix_decl_list: [
-| fix_decl_list "with" fix_decl
-| fix_decl
+one_decl_notation_list: [
+| one_decl_notation_list "and" one_decl_notation
+| one_decl_notation
 ]
 
-single_fix: [
-| fix_kw fix_decl
+one_decl_notation: [
+| string ":=" term1_extended ident_opt3
 ]
 
-fix_kw: [
-| "fix"
-| "cofix"
+ident_opt3: [
+| ":" ident
+| empty
 ]
 
-fix_decl: [
-| ident binders_fixannot type_cstr ":=" operconstr200
+record_binder: [
+| name
+| name record_binder_body
 ]
 
-match_constr: [
-| "match" case_item_list_comma case_type_opt "with" branches "end"
+record_binder_body: [
+| binders_opt of_type_with_opt_coercion term
+| binders_opt of_type_with_opt_coercion term ":=" term
+| binders_opt ":=" term
 ]
 
-case_item_list_comma: [
-| case_item_list_comma "," case_item
-| case_item
+of_type_with_opt_coercion: [
+| ":>>"
+| ":>"
+| ":"
 ]
 
-case_type_opt: [
-| case_type
+num_opt2: [
+| "|" num
 | empty
 ]
 
-case_item: [
-| operconstr100 as_opt in_opt
-]
-
-as_opt2: [
-| as_opt case_type
+quoted_attributes_list_opt: [
+| quoted_attributes_list_opt "#[" attribute_list_comma_opt "]"
 | empty
 ]
 
-in_opt: [
-| "in" pattern200
+attribute_list_comma_opt: [
+| attribute_list_comma
 | empty
 ]
 
-case_type: [
-| "return" operconstr100
+attribute_list_comma: [
+| attribute_list_comma "," attribute
+| attribute
 ]
 
-return_type: [
-| as_opt2
+attribute: [
+| ident attribute_value
 ]
 
-as_opt3: [
-| "as" dirpath
+attribute_value: [
+| "=" string
+| "(" attribute_list_comma_opt ")"
 | empty
 ]
 
-branches: [
-| or_opt eqn_list_or_opt
-]
-
-mult_pattern: [
-| pattern200_list_comma
-]
-
-pattern200_list_comma: [
-| pattern200_list_comma "," pattern200
-| pattern200
+qualid: [
+| qualid field
+| ident
 ]
 
-eqn: [
-| mult_pattern_list_or "=>" lconstr
+field: [
+| "." ident
 ]
 
-mult_pattern_list_or: [
-| mult_pattern_list_or "|" mult_pattern
-| mult_pattern
+sort: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+| "Type" "@{" "_" "}"
+| "Type" "@{" universe "}"
 ]
 
-record_pattern: [
-| global ":=" pattern200
+universe: [
+| "max" "(" universe_exprs_comma ")"
+| universe_expr
 ]
 
-record_patterns: [
-| record_pattern ";" record_patterns
-| record_pattern ";"
-| record_pattern
-| empty
+universe_exprs_comma: [
+| universe_exprs_comma "," universe_expr
+| universe_expr
 ]
 
-pattern200: [
-| pattern100
+universe_expr: [
+| universe_name universe_increment_opt
 ]
 
-pattern100: [
-| pattern99 ":" binder_constr
-| pattern99 ":" operconstr100
-| pattern99
+universe_name: [
+| qualid
+| "Set"
+| "Prop"
 ]
 
-pattern99: [
-| pattern90
+universe_increment_opt: [
+| "+" num
+| empty
 ]
 
-pattern90: [
-| pattern10
+universe_annot_opt: [
+| "@{" universe_levels_opt "}"
+| empty
 ]
 
-pattern10: [
-| pattern1 "as" name
-| pattern1 pattern1_list
-| "@" reference pattern1_list_opt
-| pattern1
+universe_levels_opt: [
+| universe_levels_opt universe_level
+| empty
 ]
 
-pattern1_list: [
-| pattern1_list pattern1
-| pattern1
+universe_level: [
+| "Set"
+| "Prop"
+| "Type"
+| "_"
+| qualid
 ]
 
-pattern1_list_opt: [
-| pattern1_list_opt pattern1
-| empty
+term_fix: [
+| single_fix
+| single_fix "with" fix_bodies "for" ident
 ]
 
-pattern1: [
-| pattern0 "%" IDENT
-| pattern0
+single_fix: [
+| "fix" fix_body
+| "cofix" fix_body
 ]
 
-pattern0: [
-| reference
-| "{|" record_patterns bar_cbrace
-| "_"
-| "(" pattern200 ")"
-| "(" pattern200 "|" pattern200_list_or ")"
-| NUMERAL
-| string
+fix_bodies: [
+| fix_bodies "with" fix_body
+| fix_body
 ]
 
-pattern200_list_or: [
-| pattern200_list_or "|" pattern200
-| pattern200
+fix_body: [
+| ident binders_opt fixannot_opt colon_term_opt ":=" term
 ]
 
-impl_ident_tail: [
-| "}"
-| name_list ":" lconstr "}"
-| name_list "}"
-| ":" lconstr "}"
+fixannot_opt: [
+| fixannot
+| empty
 ]
 
 fixannot: [
 | "{" "struct" ident "}"
-| "{" "wf" term ident "}"
-| "{" "measure" term ident_opt term_opt "}"
-| "{" "struct" name "}"
-| empty
+| "{" "wf" term1_extended ident "}"
+| "{" "measure" term1_extended ident_opt term1_extended_opt "}"
 ]
 
-term_opt: [
-| term
-| empty
+term1_extended: [
+| term1
+| "@" qualid universe_annot_opt
 ]
 
-impl_name_head: [
+ident_opt: [
+| ident
 | empty
 ]
 
-binders_fixannot: [
-| impl_name_head impl_ident_tail binders_fixannot
-| fixannot
-| binder binders_fixannot
+term1_extended_opt: [
+| term1_extended
 | empty
 ]
 
-open_binders: [
-| name name_list_opt ":" lconstr
-| name name_list_opt binders
-| name ".." name
-| closed_binder binders
-]
-
-binders: [
-| binder_list_opt
+term_let: [
+| "let" name colon_term_opt ":=" term "in" term
+| "let" name binders colon_term_opt ":=" term "in" term
+| "let" single_fix "in" term
+| "let" names_tuple as_return_type_opt ":=" term "in" term
+| "let" "'" pattern ":=" term return_type_opt "in" term
+| "let" "'" pattern "in" pattern ":=" term return_type "in" term
 ]
 
-binder_list_opt: [
-| binder_list_opt binder
+colon_term_opt: [
+| ":" term
 | empty
 ]
 
-binder: [
-| name
-| closed_binder
+names_tuple: [
+| "(" names_comma ")"
+| "()"
 ]
 
-typeclass_constraint: [
-| "!" operconstr200
-| "{" name "}" ":" exclam_opt operconstr200
-| name_colon exclam_opt operconstr200
-| operconstr200
+names_comma: [
+| names_comma "," name
+| name
 ]
 
-type_cstr: [
-| lconstr_opt
-| ":" lconstr
-| empty
+open_binders: [
+| names ":" term
+| binders
 ]
 
-preident: [
-| IDENT
+names: [
+| names name
+| name
 ]
 
-pattern_identref: [
-| "?" ident
+name: [
+| "_"
+| ident
 ]
 
-var: [
-| ident
+binders: [
+| binders binder
+| binder
 ]
 
-field: [
-| FIELD
+binder: [
+| name
+| "(" names ":" term ")"
+| "(" name colon_term_opt ":=" term ")"
+| "{" name "}"
+| "{" names colon_term_opt "}"
+| "`(" typeclass_constraints_comma ")"
+| "`{" typeclass_constraints_comma "}"
+| "'" pattern0
+| "(" name ":" term "|" term ")"
 ]
 
-fields: [
-| field fields
-| field
+typeclass_constraints_comma: [
+| typeclass_constraints_comma "," typeclass_constraint
+| typeclass_constraint
 ]
 
-fullyqualid: [
-| ident fields
-| ident
+typeclass_constraint: [
+| exclam_opt term
+| "{" name "}" ":" exclam_opt term
+| name ":" exclam_opt term
 ]
 
-basequalid: [
-| ident fields
-| ident
+exclam_opt: [
+| "!"
+| empty
 ]
 
-name: [
-| "_"
-| ident
+term_cast: [
+| term10 "<:" term
+| term10 "<<:" term
+| term10 ":" term
+| term10 ":>"
 ]
 
-reference: [
-| ident fields
-| ident
+term_match: [
+| "match" case_items_comma return_type_opt "with" or_opt eqns_or_opt "end"
 ]
 
-by_notation: [
-| ne_string IDENT_opt
+case_items_comma: [
+| case_items_comma "," case_item
+| case_item
 ]
 
-IDENT_opt: [
-| "%" IDENT
+return_type_opt: [
+| return_type
 | empty
 ]
 
-smart_global: [
-| reference
-| by_notation
+as_return_type_opt: [
+| as_name_opt return_type
+| empty
 ]
 
-qualid: [
-| basequalid
+return_type: [
+| "return" term100
 ]
 
-ne_string: [
-| STRING
+case_item: [
+| term100 as_name_opt in_opt
 ]
 
-ne_lstring: [
-| ne_string
+as_name_opt: [
+| "as" name
+| empty
 ]
 
-dirpath: [
-| ident field_list_opt
+in_opt: [
+| "in" pattern
+| empty
 ]
 
-field_list_opt: [
-| field_list_opt field
+or_opt: [
+| "|"
 | empty
 ]
 
-string: [
-| STRING
+eqns_or_opt: [
+| eqns_or
+| empty
 ]
 
-lstring: [
-| string
+eqns_or: [
+| eqns_or "|" eqn
+| eqn
 ]
 
-integer: [
-| NUMERAL
-| "-" NUMERAL
+eqn: [
+| patterns_comma_list_or "=>" term
 ]
 
-natural: [
-| NUMERAL
+patterns_comma_list_or: [
+| patterns_comma_list_or "|" patterns_comma
+| patterns_comma
 ]
 
-bigint: [
-| NUMERAL
+patterns_comma: [
+| patterns_comma "," pattern
+| pattern
 ]
 
-bar_cbrace: [
-| "|" "}"
+pattern: [
+| pattern10 ":" term
+| pattern10
 ]
 
-vernac_control: [
-| "Time" vernac_control
-| "Redirect" ne_string vernac_control
-| "Timeout" natural vernac_control
-| "Fail" vernac_control
-| decorated_vernac
+pattern10: [
+| pattern1 "as" name
+| pattern1_list
+| "@" qualid pattern1_list_opt
+| pattern1
 ]
 
-decorated_vernac: [
-| quoted_attributes_list_opt vernac
+pattern1_list: [
+| pattern1_list pattern1
+| pattern1
 ]
 
-quoted_attributes_list_opt: [
-| quoted_attributes_list_opt quoted_attributes
+pattern1_list_opt: [
+| pattern1_list
 | empty
 ]
 
-quoted_attributes: [
-| "#[" attribute_list_comma_opt "]"
+pattern1: [
+| pattern0 "%" ident
+| pattern0
 ]
 
-attribute_list_comma_opt: [
-| attribute_list_comma
-| empty
+pattern0: [
+| qualid
+| "{|" record_patterns_opt "|}"
+| "_"
+| "(" patterns_or ")"
+| numeral
+| string
 ]
 
-attribute_list_comma: [
-| attribute_list_comma "," attribute
-| attribute
+patterns_or: [
+| patterns_or "|" pattern
+| pattern
 ]
 
-attribute: [
-| ident attribute_value
+record_patterns_opt: [
+| record_patterns_opt ";" record_pattern
+| record_pattern
+| empty
 ]
 
-attribute_value: [
-| "=" string
-| "(" attribute_list_comma_opt ")"
-| empty
+record_pattern: [
+| qualid ":=" pattern
 ]
 
 vernac: [
@@ -620,44 +558,51 @@ vernac_aux: [
 | gallina "."
 | gallina_ext "."
 | command "."
+| tactic_mode "."
 | syntax "."
 | subprf
-| command_entry
-]
-
-noedit_mode: [
 | query_command
 ]
 
 subprf: [
-| BULLET
+| bullet
 | "{"
 | "}"
 ]
 
 gallina: [
-| thm_token ident_decl binders ":" lconstr with_list_opt
+| thm_token ident_decl binders_opt ":" term with_list_opt
 | assumption_token inline assum_list
 | assumptions_token inline assum_list
 | def_token ident_decl def_body
 | "Let" ident def_body
 | cumulativity_token_opt private_token finite_token inductive_definition_list
-| "Fixpoint" rec_definition_list
-| "Let" "Fixpoint" rec_definition_list
-| "CoFixpoint" corec_definition_list
-| "Let" "CoFixpoint" corec_definition_list
+| "Fixpoint" fix_definition_list
+| "Let" "Fixpoint" fix_definition_list
+| "CoFixpoint" cofix_definition_list
+| "Let" "CoFixpoint" cofix_definition_list
 | "Scheme" scheme_list
 | "Combined" "Scheme" ident "from" ident_list_comma
-| "Register" global "as" qualid
-| "Register" "Inline" global
-| "Primitive" ident lconstr_opt ":=" register_token
+| "Register" qualid "as" qualid
+| "Register" "Inline" qualid
+| "Primitive" ident term_opt ":=" register_token
 | "Universe" ident_list
 | "Universes" ident_list
 | "Constraint" univ_constraint_list_comma
 ]
 
+term_opt: [
+| ":" term
+| empty
+]
+
+univ_constraint_list_comma: [
+| univ_constraint_list_comma "," univ_constraint
+| univ_constraint
+]
+
 with_list_opt: [
-| with_list_opt "with" ident_decl binders ":" lconstr
+| with_list_opt "with" ident_decl binders_opt ":" term
 | empty
 ]
 
@@ -671,14 +616,23 @@ inductive_definition_list: [
 | inductive_definition
 ]
 
-rec_definition_list: [
-| rec_definition_list "with" rec_definition
-| rec_definition
+fix_definition_list: [
+| fix_definition_list "with" fix_definition
+| fix_definition
 ]
 
-corec_definition_list: [
-| corec_definition_list "with" corec_definition
-| corec_definition
+fix_definition: [
+| ident_decl binders_opt fixannot_opt colon_term_opt term_opt2 decl_notation
+]
+
+term_opt2: [
+| ":=" term
+| empty
+]
+
+cofix_definition_list: [
+| cofix_definition_list "with" cofix_definition
+| cofix_definition
 ]
 
 scheme_list: [
@@ -691,23 +645,10 @@ ident_list_comma: [
 | ident
 ]
 
-univ_constraint_list_comma: [
-| univ_constraint_list_comma "," univ_constraint
-| univ_constraint
-]
-
-lconstr_opt2: [
-| ":=" lconstr
-| empty
-]
-
 register_token: [
 | register_prim_token
-| register_type_token
-]
-
-register_type_token: [
 | "#int63_type"
+| "#float64_type"
 ]
 
 register_prim_token: [
@@ -735,6 +676,24 @@ register_prim_token: [
 | "#int63_lt"
 | "#int63_le"
 | "#int63_compare"
+| "#float64_opp"
+| "#float64_abs"
+| "#float64_eq"
+| "#float64_lt"
+| "#float64_le"
+| "#float64_compare"
+| "#float64_classify"
+| "#float64_add"
+| "#float64_sub"
+| "#float64_mul"
+| "#float64_div"
+| "#float64_sqrt"
+| "#float64_of_int63"
+| "#float64_normfr_mantissa"
+| "#float64_frshiftexp"
+| "#float64_ldshiftexp"
+| "#float64_next_up"
+| "#float64_next_down"
 ]
 
 thm_token: [
@@ -770,7 +729,7 @@ assumptions_token: [
 ]
 
 inline: [
-| "Inline" "(" natural ")"
+| "Inline" "(" num ")"
 | "Inline"
 | empty
 ]
@@ -785,30 +744,6 @@ lt_alt: [
 | "<="
 ]
 
-univ_decl: [
-| "@{" ident_list_opt plus_opt univ_constraint_alt
-]
-
-plus_opt: [
-| "+"
-| empty
-]
-
-univ_constraint_alt: [
-| "|" univ_constraint_list_comma_opt plus_opt "}"
-| rbrace_alt
-]
-
-univ_constraint_list_comma_opt: [
-| univ_constraint_list_comma
-| empty
-]
-
-rbrace_alt: [
-| "}"
-| bar_cbrace
-]
-
 ident_decl: [
 | ident univ_decl_opt
 ]
@@ -833,9 +768,9 @@ private_token: [
 ]
 
 def_body: [
-| binders ":=" reduce lconstr
-| binders ":" lconstr ":=" reduce lconstr
-| binders ":" lconstr
+| binders_opt ":=" reduce term
+| binders_opt ":" term ":=" reduce term
+| binders_opt ":" term
 ]
 
 reduce: [
@@ -843,27 +778,70 @@ reduce: [
 | empty
 ]
 
-one_decl_notation: [
-| ne_lstring ":=" term IDENT_opt2
+red_expr: [
+| "red"
+| "hnf"
+| "simpl" delta_flag ref_or_pattern_occ_opt
+| "cbv" strategy_flag
+| "cbn" strategy_flag
+| "lazy" strategy_flag
+| "compute" delta_flag
+| "vm_compute" ref_or_pattern_occ_opt
+| "native_compute" ref_or_pattern_occ_opt
+| "unfold" unfold_occ_list_comma
+| "fold" term1_extended_list
+| "pattern" pattern_occ_list_comma
+| ident
 ]
 
-IDENT_opt2: [
-| ":" IDENT
-| empty
+strategy_flag: [
+| red_flags_list
+| delta_flag
+]
+
+red_flags_list: [
+| red_flags_list red_flags
+| red_flags
 ]
 
-decl_sep: [
-| "and"
+red_flags: [
+| "beta"
+| "iota"
+| "match"
+| "fix"
+| "cofix"
+| "zeta"
+| "delta" delta_flag
 ]
 
-decl_notation: [
-| "where" one_decl_notation_list
+delta_flag: [
+| "-" "[" smart_global_list "]"
+| "[" smart_global_list "]"
 | empty
 ]
 
-one_decl_notation_list: [
-| one_decl_notation_list decl_sep one_decl_notation
-| one_decl_notation
+ref_or_pattern_occ_opt: [
+| ref_or_pattern_occ
+| empty
+]
+
+ref_or_pattern_occ: [
+| smart_global occs
+| term1_extended occs
+]
+
+unfold_occ_list_comma: [
+| unfold_occ_list_comma "," unfold_occ
+| unfold_occ
+]
+
+unfold_occ: [
+| smart_global occs
+]
+
+pattern_occ_list_comma: [
+| pattern_occ_list_comma "," pattern_occ
+| pattern_occ
 ]
 
 opt_constructors_or_fields: [
@@ -872,7 +850,12 @@ opt_constructors_or_fields: [
 ]
 
 inductive_definition: [
-| opt_coercion ident_decl binders lconstr_opt opt_constructors_or_fields decl_notation
+| opt_coercion ident_decl binders_opt term_opt opt_constructors_or_fields decl_notation
+]
+
+opt_coercion: [
+| ">"
+| empty
 ]
 
 constructor_list_or_record_decl: [
@@ -894,52 +877,6 @@ constructor_list_or_opt: [
 | empty
 ]
 
-opt_coercion: [
-| ">"
-| empty
-]
-
-rec_definition: [
-| ident_decl binders_fixannot type_cstr lconstr_opt2 decl_notation
-]
-
-corec_definition: [
-| ident_decl binders type_cstr lconstr_opt2 decl_notation
-]
-
-lconstr_opt: [
-| ":" lconstr
-| empty
-]
-
-scheme: [
-| scheme_kind
-| ident ":=" scheme_kind
-]
-
-scheme_kind: [
-| "Induction" "for" smart_global "Sort" sort_family
-| "Minimality" "for" smart_global "Sort" sort_family
-| "Elimination" "for" smart_global "Sort" sort_family
-| "Case" "for" smart_global "Sort" sort_family
-| "Equality" "for" smart_global
-]
-
-record_field: [
-| quoted_attributes_list_opt record_binder natural_opt2 decl_notation
-]
-
-record_binder_body: [
-| binders of_type_with_opt_coercion lconstr
-| binders of_type_with_opt_coercion lconstr ":=" lconstr
-| binders ":=" lconstr
-]
-
-record_binder: [
-| name
-| name record_binder_body
-]
-
 assum_list: [
 | assum_coe_list
 | simple_assum_coe
@@ -955,7 +892,7 @@ assum_coe: [
 ]
 
 simple_assum_coe: [
-| ident_decl_list of_type_with_opt_coercion lconstr
+| ident_decl_list of_type_with_opt_coercion term
 ]
 
 ident_decl_list: [
@@ -964,11 +901,11 @@ ident_decl_list: [
 ]
 
 constructor_type: [
-| binders of_type_with_opt_coercion_opt
+| binders_opt of_type_with_opt_coercion_opt
 ]
 
 of_type_with_opt_coercion_opt: [
-| of_type_with_opt_coercion lconstr
+| of_type_with_opt_coercion term
 | empty
 ]
 
@@ -976,95 +913,135 @@ constructor: [
 | ident constructor_type
 ]
 
-of_type_with_opt_coercion: [
-| ":>>"
-| ":>" ">"
-| ":>"
-| ":" ">" ">"
-| ":" ">"
-| ":"
+cofix_definition: [
+| ident_decl binders_opt colon_term_opt term_opt2 decl_notation
+]
+
+scheme: [
+| scheme_kind
+| ident ":=" scheme_kind
+]
+
+scheme_kind: [
+| "Induction" "for" smart_global "Sort" sort_family
+| "Minimality" "for" smart_global "Sort" sort_family
+| "Elimination" "for" smart_global "Sort" sort_family
+| "Case" "for" smart_global "Sort" sort_family
+| "Equality" "for" smart_global
+]
+
+sort_family: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+]
+
+smart_global: [
+| qualid
+| by_notation
+]
+
+by_notation: [
+| string ident_opt2
+]
+
+ident_opt2: [
+| "%" ident
+| empty
 ]
 
 gallina_ext: [
 | "Module" export_token ident module_binder_list_opt of_module_type is_module_expr
-| "Module" "Type" ident module_binder_list_opt check_module_types is_module_type
+| "Module" "Type" ident module_binder_list_opt module_type_inl_list_opt is_module_type
 | "Declare" "Module" export_token ident module_binder_list_opt ":" module_type_inl
 | "Section" ident
 | "Chapter" ident
 | "End" ident
 | "Collection" ident ":=" section_subset_expr
-| "Require" export_token global_list
-| "From" global "Require" export_token global_list
-| "Import" global_list
-| "Export" global_list
-| "Include" module_type_inl ext_module_expr_list_opt
-| "Include" "Type" module_type_inl ext_module_type_list_opt
+| "Require" export_token qualid_list
+| "From" qualid "Require" export_token qualid_list
+| "Import" qualid_list
+| "Export" qualid_list
+| "Include" module_type_inl module_expr_inl_list_opt
+| "Include" "Type" module_type_inl module_type_inl_list_opt
 | "Transparent" smart_global_list
 | "Opaque" smart_global_list
 | "Strategy" strategy_level_list
-| "Canonical" Structure_opt global univ_decl_opt2
+| "Canonical" Structure_opt qualid univ_decl_opt2
 | "Canonical" Structure_opt by_notation
-| "Coercion" global univ_decl_opt def_body
+| "Coercion" qualid univ_decl_opt def_body
 | "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr
-| "Coercion" global ":" class_rawexpr ">->" class_rawexpr
+| "Coercion" qualid ":" class_rawexpr ">->" class_rawexpr
 | "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
-| "Context" binder_list
-| "Instance" instance_name ":" operconstr200 hint_info record_declaration_opt
-| "Existing" "Instance" global hint_info
-| "Existing" "Instances" global_list natural_opt2
-| "Existing" "Class" global
+| "Context" binders
+| "Instance" instance_name ":" term hint_info fields_def_opt
+| "Existing" "Instance" qualid hint_info
+| "Existing" "Instances" qualid_list num_opt2
+| "Existing" "Class" qualid
 | "Arguments" smart_global argument_spec_block_list_opt more_implicits_block_opt arguments_modifier_opt
 | "Implicit" "Type" reserv_list
 | "Implicit" "Types" reserv_list
 | "Generalizable" All_alt
-| "Export" "Set" option_table option_setting
-| "Export" "Unset" option_table
-| "Import" "Prenex" "Implicits"      (* ssr plugin *)
+| "Export" "Set" ident_list option_setting
+| "Export" "Unset" ident_list
 ]
 
-module_binder_list_opt: [
-| module_binder_list_opt module_binder
-| empty
+smart_global_list: [
+| smart_global_list smart_global
+| smart_global
 ]
 
-ext_module_expr_list_opt: [
-| ext_module_expr_list_opt ext_module_expr
+num_opt: [
+| num
 | empty
 ]
 
-ext_module_type_list_opt: [
-| ext_module_type_list_opt ext_module_type
+qualid_list: [
+| qualid_list qualid
+| qualid
+]
+
+option_setting: [
 | empty
+| int
+| string
 ]
 
-strategy_level_list: [
-| strategy_level_list strategy_level "[" smart_global_list "]"
-| strategy_level "[" smart_global_list "]"
+class_rawexpr: [
+| "Funclass"
+| "Sortclass"
+| smart_global
 ]
 
-Structure_opt: [
-| "Structure"
+hint_info: [
+| "|" num_opt term1_extended_opt
 | empty
 ]
 
-univ_decl_opt: [
-| univ_decl
+module_binder_list_opt: [
+| module_binder_list_opt "(" export_token ident_list ":" module_type_inl ")"
 | empty
 ]
 
-binder_list: [
-| binder_list binder
-| binder
+module_type_inl_list_opt: [
+| module_type_inl_list_opt module_type_inl
+| empty
 ]
 
-record_declaration_opt: [
-| ":=" "{" record_declaration "}"
-| ":=" lconstr
+module_expr_inl_list_opt: [
+| module_expr_inl_list_opt module_expr_inl
 | empty
 ]
 
-natural_opt: [
-| natural
+strategy_level_list: [
+| strategy_level_list strategy_level "[" smart_global_list "]"
+| strategy_level "[" smart_global_list "]"
+]
+
+fields_def_opt: [
+| ":=" "{" fields_def "}"
+| ":=" term
 | empty
 ]
 
@@ -1114,50 +1091,54 @@ univ_decl_opt2: [
 | empty
 ]
 
-export_token: [
-| "Import"
-| "Export"
+univ_decl_opt: [
+| "@{" ident_list_opt plus_opt univ_constraint_alt
 | empty
 ]
 
-ext_module_type: [
-| "<+" module_type_inl
+plus_opt: [
+| "+"
+| empty
 ]
 
-ext_module_expr: [
-| "<+" module_expr_inl
+univ_constraint_alt: [
+| "|" univ_constraint_list_comma_opt plus_opt "}"
+| rbrace_alt
 ]
 
-check_module_type: [
-| "<:" module_type_inl
+univ_constraint_list_comma_opt: [
+| univ_constraint_list_comma
+| empty
 ]
 
-check_module_types: [
-| check_module_type_list_opt
+rbrace_alt: [
+| "}"
+| "|}"
 ]
 
-check_module_type_list_opt: [
-| check_module_type_list_opt check_module_type
+export_token: [
+| "Import"
+| "Export"
 | empty
 ]
 
 of_module_type: [
 | ":" module_type_inl
-| check_module_types
+| module_type_inl_list_opt
 ]
 
 is_module_type: [
-| ":=" module_type_inl ext_module_type_list_opt
+| ":=" module_type_inl module_type_inl_list_opt
 | empty
 ]
 
 is_module_expr: [
-| ":=" module_expr_inl ext_module_expr_list_opt
+| ":=" module_expr_inl module_expr_inl_list_opt
 | empty
 ]
 
 functor_app_annot: [
-| "[" "inline" "at" "level" natural "]"
+| "[" "inline" "at" "level" num "]"
 | "[" "no" "inline" "]"
 | empty
 ]
@@ -1172,10 +1153,6 @@ module_type_inl: [
 | module_type functor_app_annot
 ]
 
-module_binder: [
-| "(" export_token ident_list ":" module_type_inl ")"
-]
-
 module_expr: [
 | module_expr_atom
 | module_expr module_expr_atom
@@ -1186,11 +1163,6 @@ module_expr_atom: [
 | "(" module_expr ")"
 ]
 
-with_declaration: [
-| "Definition" fullyqualid univ_decl_opt ":=" lconstr
-| "Module" fullyqualid ":=" qualid
-]
-
 module_type: [
 | qualid
 | "(" module_type ")"
@@ -1198,108 +1170,45 @@ module_type: [
 | module_type "with" with_declaration
 ]
 
-section_subset_expr: [
-| starredidentref_list_opt
-| ssexpr35
-]
-
-starredidentref_list_opt: [
-| starredidentref_list_opt starredidentref
-| empty
-]
-
-starredidentref: [
-| ident
-| ident "*"
-| "Type"
-| "Type" "*"
-]
-
-ssexpr35: [
-| "-" ssexpr50
-| ssexpr50
-]
-
-ssexpr50: [
-| ssexpr0 "-" ssexpr0
-| ssexpr0 "+" ssexpr0
-| ssexpr0
-]
-
-ssexpr0: [
-| starredidentref
-| "(" starredidentref_list_opt ")"
-| "(" starredidentref_list_opt ")" "*"
-| "(" ssexpr35 ")"
-| "(" ssexpr35 ")" "*"
-]
-
-arguments_modifier: [
-| "simpl" "nomatch"
-| "simpl" "never"
-| "default" "implicits"
-| "clear" "implicits"
-| "clear" "scopes"
-| "clear" "bidirectionality" "hint"
-| "rename"
-| "assert"
-| "extra" "scopes"
-| "clear" "scopes" "and" "implicits"
-| "clear" "implicits" "and" "scopes"
-]
-
-scope: [
-| "%" IDENT
-]
-
-argument_spec: [
-| exclam_opt name scope_opt
-]
-
-exclam_opt: [
-| "!"
-| empty
-]
-
-scope_opt: [
-| scope
-| empty
+with_declaration: [
+| "Definition" qualid univ_decl_opt ":=" term
+| "Module" qualid ":=" qualid
 ]
 
 argument_spec_block: [
-| argument_spec
+| exclam_opt name scope_delimiter_opt
 | "/"
 | "&"
-| "(" argument_spec_list ")" scope_opt
-| "[" argument_spec_list "]" scope_opt
-| "{" argument_spec_list "}" scope_opt
+| "(" scope_delimiter_list ")" scope_delimiter_opt
+| "[" scope_delimiter_list "]" scope_delimiter_opt
+| "{" scope_delimiter_list "}" scope_delimiter_opt
+]
+
+scope_delimiter_opt: [
+| "%" ident
+| empty
 ]
 
-argument_spec_list: [
-| argument_spec_list argument_spec
-| argument_spec
+scope_delimiter_list: [
+| scope_delimiter_list scope_delimiter_opt
+| scope_delimiter_opt
 ]
 
 more_implicits_block: [
 | name
-| "[" name_list "]"
-| "{" name_list "}"
+| "[" names "]"
+| "{" names "}"
 ]
 
 strategy_level: [
 | "expand"
 | "opaque"
-| integer
+| int
 | "transparent"
 ]
 
 instance_name: [
-| ident_decl binders
-| empty
-]
-
-hint_info: [
-| "|" natural_opt constr_pattern_opt
+| ident_decl binders_opt
 | empty
 ]
 
@@ -1318,64 +1227,83 @@ reserv_tuple: [
 ]
 
 simple_reserv: [
-| ident_list ":" lconstr
+| ident_list ":" term
+]
+
+arguments_modifier: [
+| "simpl" "nomatch"
+| "simpl" "never"
+| "default" "implicits"
+| "clear" "implicits"
+| "clear" "scopes"
+| "clear" "bidirectionality" "hint"
+| "rename"
+| "assert"
+| "extra" "scopes"
+| "clear" "scopes" "and" "implicits"
+| "clear" "implicits" "and" "scopes"
+]
+
+Structure_opt: [
+| "Structure"
+| empty
 ]
 
 command: [
+| "Goal" term
 | "Comments" comment_list_opt
-| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info
-| "Declare" "Scope" IDENT
+| "Declare" "Instance" ident_decl binders_opt ":" term hint_info
+| "Declare" "Scope" ident
 | "Pwd"
 | "Cd"
-| "Cd" ne_string
-| "Load" Verbose_opt ne_string_alt
-| "Declare" "ML" "Module" ne_string_list
+| "Cd" string
+| "Load" Verbose_opt string_alt
+| "Declare" "ML" "Module" string_list
 | "Locate" locatable
-| "Add" "LoadPath" ne_string as_dirpath
-| "Add" "Rec" "LoadPath" ne_string as_dirpath
-| "Remove" "LoadPath" ne_string
-| "AddPath" ne_string "as" as_dirpath
-| "AddRecPath" ne_string "as" as_dirpath
-| "DelPath" ne_string
-| "Type" lconstr
+| "Add" "LoadPath" string as_dirpath
+| "Add" "Rec" "LoadPath" string as_dirpath
+| "Remove" "LoadPath" string
+| "AddPath" string "as" as_dirpath
+| "AddRecPath" string "as" as_dirpath
+| "DelPath" string
+| "Type" term
 | "Print" printable
 | "Print" smart_global univ_name_list_opt
-| "Print" "Module" "Type" global
-| "Print" "Module" global
+| "Print" "Module" "Type" qualid
+| "Print" "Module" qualid
 | "Print" "Namespace" dirpath
-| "Inspect" natural
-| "Add" "ML" "Path" ne_string
-| "Add" "Rec" "ML" "Path" ne_string
-| "Set" option_table option_setting
-| "Unset" option_table
-| "Print" "Table" option_table
-| "Add" IDENT IDENT option_ref_value_list
-| "Add" IDENT option_ref_value_list
-| "Test" option_table "for" option_ref_value_list
-| "Test" option_table
-| "Remove" IDENT IDENT option_ref_value_list
-| "Remove" IDENT option_ref_value_list
-| "Write" "State" IDENT
-| "Write" "State" ne_string
-| "Restore" "State" IDENT
-| "Restore" "State" ne_string
+| "Inspect" num
+| "Add" "ML" "Path" string
+| "Add" "Rec" "ML" "Path" string
+| "Set" ident_list option_setting
+| "Unset" ident_list
+| "Print" "Table" ident_list
+| "Add" ident ident option_ref_value_list
+| "Add" ident option_ref_value_list
+| "Test" ident_list "for" option_ref_value_list
+| "Test" ident_list
+| "Remove" ident ident option_ref_value_list
+| "Remove" ident option_ref_value_list
+| "Write" "State" ident
+| "Write" "State" string
+| "Restore" "State" ident
+| "Restore" "State" string
 | "Reset" "Initial"
 | "Reset" ident
 | "Back"
-| "Back" natural
-| "BackTo" natural
+| "Back" num
 | "Debug" "On"
 | "Debug" "Off"
-| "Declare" "Reduction" IDENT; ":=" red_expr
-| "Declare" "Custom" "Entry" IDENT
-| "Goal" lconstr
+| "Declare" "Reduction" ident ":=" red_expr
+| "Declare" "Custom" "Entry" ident
+| "Derive" ident "SuchThat" term1_extended "As" ident      (* derive plugin *)
 | "Proof"
 | "Proof" "Mode" string
-| "Proof" lconstr
+| "Proof" term
 | "Abort"
 | "Abort" "All"
 | "Abort" ident
-| "Existential" natural constr_body
+| "Existential" num constr_body
 | "Admitted"
 | "Qed"
 | "Save" ident
@@ -1383,14 +1311,14 @@ command: [
 | "Defined" ident
 | "Restart"
 | "Undo"
-| "Undo" natural
-| "Undo" "To" natural
+| "Undo" num
+| "Undo" "To" num
 | "Focus"
-| "Focus" natural
+| "Focus" num
 | "Unfocus"
 | "Unfocused"
 | "Show"
-| "Show" natural
+| "Show" num
 | "Show" ident
 | "Show" "Existentials"
 | "Show" "Universes"
@@ -1398,47 +1326,57 @@ command: [
 | "Show" "Proof"
 | "Show" "Intro"
 | "Show" "Intros"
-| "Show" "Match" reference
+| "Show" "Match" qualid
 | "Guarded"
-| "Create" "HintDb" IDENT discriminated_opt
-| "Remove" "Hints" global_list opt_hintbases
+| "Create" "HintDb" ident discriminated_opt
+| "Remove" "Hints" qualid_list opt_hintbases
 | "Hint" hint opt_hintbases
-| "Obligation" integer "of" ident ":" lglob withtac
-| "Obligation" integer "of" ident withtac
-| "Obligation" integer ":" lglob withtac
-| "Obligation" integer withtac
+| "Obligation" int "of" ident ":" term withtac
+| "Obligation" int "of" ident withtac
+| "Obligation" int ":" term withtac
+| "Obligation" int withtac
 | "Next" "Obligation" "of" ident withtac
 | "Next" "Obligation" withtac
-| "Solve" "Obligation" integer "of" ident "with" tactic
-| "Solve" "Obligation" integer "with" tactic
-| "Solve" "Obligations" "of" ident "with" tactic
-| "Solve" "Obligations" "with" tactic
+| "Solve" "Obligation" int "of" ident "with" ltac_expr
+| "Solve" "Obligation" int "with" ltac_expr
+| "Solve" "Obligations" "of" ident "with" ltac_expr
+| "Solve" "Obligations" "with" ltac_expr
 | "Solve" "Obligations"
-| "Solve" "All" "Obligations" "with" tactic
+| "Solve" "All" "Obligations" "with" ltac_expr
 | "Solve" "All" "Obligations"
 | "Admit" "Obligations" "of" ident
 | "Admit" "Obligations"
-| "Obligation" "Tactic" ":=" tactic
+| "Obligation" "Tactic" ":=" ltac_expr
 | "Show" "Obligation" "Tactic"
 | "Obligations" "of" ident
 | "Obligations"
 | "Preterm" "of" ident
 | "Preterm"
-| "Hint" "Rewrite" orient term_list ":" preident_list_opt
-| "Hint" "Rewrite" orient term_list "using" tactic ":" preident_list_opt
-| "Hint" "Rewrite" orient term_list
-| "Hint" "Rewrite" orient term_list "using" tactic
-| "Derive" "Inversion_clear" ident "with" term "Sort" sort_family
-| "Derive" "Inversion_clear" ident "with" term
-| "Derive" "Inversion" ident "with" term "Sort" sort_family
-| "Derive" "Inversion" ident "with" term
-| "Derive" "Dependent" "Inversion" ident "with" term "Sort" sort_family
-| "Derive" "Dependent" "Inversion_clear" ident "with" term "Sort" sort_family
-| "Declare" "Left" "Step" term
-| "Declare" "Right" "Step" term
+| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Setoid" term1_extended term1_extended term1_extended "as" ident
+| "Add" "Parametric" "Setoid" binders_opt ":" term1_extended term1_extended term1_extended "as" ident
+| "Add" "Morphism" term1_extended ":" ident
+| "Declare" "Morphism" term1_extended ":" ident
+| "Add" "Morphism" term1_extended "with" "signature" term "as" ident
+| "Add" "Parametric" "Morphism" binders_opt ":" term1_extended "with" "signature" term "as" ident
 | "Grab" "Existential" "Variables"
 | "Unshelve"
-| "Declare" "Equivalent" "Keys" term term
+| "Declare" "Equivalent" "Keys" term1_extended term1_extended
 | "Print" "Equivalent" "Keys"
 | "Optimize" "Proof"
 | "Optimize" "Heap"
@@ -1446,129 +1384,143 @@ command: [
 | "Show" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
+| "Add" "InjTyp" term1_extended      (* micromega plugin *)
+| "Add" "BinOp" term1_extended      (* micromega plugin *)
+| "Add" "UnOp" term1_extended      (* micromega plugin *)
+| "Add" "CstOp" term1_extended      (* micromega plugin *)
+| "Add" "BinRel" term1_extended      (* micromega plugin *)
+| "Add" "PropOp" term1_extended      (* micromega plugin *)
+| "Add" "PropUOp" term1_extended      (* micromega plugin *)
+| "Add" "Spec" term1_extended      (* micromega plugin *)
+| "Add" "BinOpSpec" term1_extended      (* micromega plugin *)
+| "Add" "UnOpSpec" term1_extended      (* micromega plugin *)
+| "Add" "Saturate" term1_extended      (* micromega plugin *)
+| "Show" "Zify" "InjTyp"      (* micromega plugin *)
+| "Show" "Zify" "BinOp"      (* micromega plugin *)
+| "Show" "Zify" "UnOp"      (* micromega plugin *)
+| "Show" "Zify" "CstOp"      (* micromega plugin *)
+| "Show" "Zify" "BinRel"      (* micromega plugin *)
+| "Show" "Zify" "Spec"      (* micromega plugin *)
+| "Add" "Ring" ident ":" term1_extended ring_mods_opt      (* setoid_ring plugin *)
 | "Hint" "Cut" "[" hints_path "]" opthints
-| "Typeclasses" "Transparent" reference_list_opt
-| "Typeclasses" "Opaque" reference_list_opt
+| "Typeclasses" "Transparent" qualid_list_opt
+| "Typeclasses" "Opaque" qualid_list_opt
 | "Typeclasses" "eauto" ":=" debug eauto_search_strategy int_opt
-| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident
-| "Add" "Relation" term term "reflexivity" "proved" "by" term "as" ident
-| "Add" "Relation" term term "as" ident
-| "Add" "Relation" term term "symmetry" "proved" "by" term "as" ident
-| "Add" "Relation" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident
-| "Add" "Relation" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident
-| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident
-| "Add" "Relation" term term "transitivity" "proved" "by" term "as" ident
-| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident
-| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "as" ident
-| "Add" "Parametric" "Relation" binders ":" term term "as" ident
-| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "as" ident
-| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident
-| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident
-| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident
-| "Add" "Parametric" "Relation" binders ":" term term "transitivity" "proved" "by" term "as" ident
-| "Add" "Setoid" term term term "as" ident
-| "Add" "Parametric" "Setoid" binders ":" term term term "as" ident
-| "Add" "Morphism" term ":" ident
-| "Declare" "Morphism" term ":" ident
-| "Add" "Morphism" term "with" "signature" lconstr "as" ident
-| "Add" "Parametric" "Morphism" binders ":" term "with" "signature" lconstr "as" ident
-| "Print" "Rewrite" "HintDb" preident
-| "Proof" "with" tactic using_opt
+| "Print" "Rewrite" "HintDb" ident
+| "Proof" "with" ltac_expr using_opt
 | "Proof" "using" section_subset_expr with_opt
-| "Tactic" "Notation" ltac_tactic_level_opt ltac_production_item_list ":=" tactic
-| "Print" "Ltac" reference
-| "Locate" "Ltac" reference
-| "Ltac" ltac_tacdef_body_list
+| "Tactic" "Notation" ltac_tactic_level_opt ltac_production_item_list ":=" ltac_expr
+| "Print" "Ltac" qualid
+| "Locate" "Ltac" qualid
+| "Ltac" tacdef_body_list
 | "Print" "Ltac" "Signatures"
-| "String" "Notation" reference reference reference ":" ident
-| "Set" "Firstorder" "Solver" tactic
+| "Set" "Firstorder" "Solver" ltac_expr
 | "Print" "Firstorder" "Solver"
-| "Numeral" "Notation" reference reference reference ":" ident numnotoption
-| "Derive" ident "SuchThat" term "As" ident      (* derive plugin *)
-| "Extraction" global      (* extraction plugin *)
-| "Recursive" "Extraction" global_list      (* extraction plugin *)
-| "Extraction" string global_list      (* extraction plugin *)
-| "Extraction" "TestCompile" global_list      (* extraction plugin *)
-| "Separate" "Extraction" global_list      (* extraction plugin *)
+| "Extraction" qualid      (* extraction plugin *)
+| "Recursive" "Extraction" qualid_list      (* extraction plugin *)
+| "Extraction" string qualid_list      (* extraction plugin *)
+| "Extraction" "TestCompile" qualid_list      (* extraction plugin *)
+| "Separate" "Extraction" qualid_list      (* extraction plugin *)
 | "Extraction" "Library" ident      (* extraction plugin *)
 | "Recursive" "Extraction" "Library" ident      (* extraction plugin *)
 | "Extraction" "Language" language      (* extraction plugin *)
-| "Extraction" "Inline" global_list      (* extraction plugin *)
-| "Extraction" "NoInline" global_list      (* extraction plugin *)
+| "Extraction" "Inline" qualid_list      (* extraction plugin *)
+| "Extraction" "NoInline" qualid_list      (* extraction plugin *)
 | "Print" "Extraction" "Inline"      (* extraction plugin *)
 | "Reset" "Extraction" "Inline"      (* extraction plugin *)
-| "Extraction" "Implicit" global "[" int_or_id_list_opt "]"      (* extraction plugin *)
+| "Extraction" "Implicit" qualid "[" int_or_id_list_opt "]"      (* extraction plugin *)
 | "Extraction" "Blacklist" ident_list      (* extraction plugin *)
 | "Print" "Extraction" "Blacklist"      (* extraction plugin *)
 | "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
-| "Extract" "Constant" global string_list_opt "=>" mlname      (* extraction plugin *)
-| "Extract" "Inlined" "Constant" global "=>" mlname      (* extraction plugin *)
-| "Extract" "Inductive" global "=>" mlname "[" mlname_list_opt "]" string_opt      (* extraction plugin *)
+| "Extract" "Constant" qualid string_list_opt "=>" mlname      (* extraction plugin *)
+| "Extract" "Inlined" "Constant" qualid "=>" mlname      (* extraction plugin *)
+| "Extract" "Inductive" qualid "=>" mlname "[" mlname_list_opt "]" string_opt      (* extraction plugin *)
 | "Show" "Extraction"      (* extraction plugin *)
-| "Function" function_rec_definition_loc_list      (* funind plugin *)
+| "Function" fix_definition_list      (* funind plugin *)
 | "Functional" "Scheme" fun_scheme_arg_list      (* funind plugin *)
 | "Functional" "Case" fun_scheme_arg      (* funind plugin *)
-| "Generate" "graph" "for" reference      (* funind plugin *)
-| "Add" "Ring" ident ":" term ring_mods_opt      (* setoid_ring plugin *)
+| "Generate" "graph" "for" qualid      (* funind plugin *)
+| "Hint" "Rewrite" orient term1_extended_list ":" ident_list_opt
+| "Hint" "Rewrite" orient term1_extended_list "using" ltac_expr ":" ident_list_opt
+| "Hint" "Rewrite" orient term1_extended_list
+| "Hint" "Rewrite" orient term1_extended_list "using" ltac_expr
+| "Derive" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
+| "Derive" "Inversion_clear" ident "with" term1_extended
+| "Derive" "Inversion" ident "with" term1_extended "Sort" sort_family
+| "Derive" "Inversion" ident "with" term1_extended
+| "Derive" "Dependent" "Inversion" ident "with" term1_extended "Sort" sort_family
+| "Derive" "Dependent" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
+| "Declare" "Left" "Step" term1_extended
+| "Declare" "Right" "Step" term1_extended
 | "Print" "Rings"      (* setoid_ring plugin *)
-| "Add" "Field" ident ":" term field_mods_opt      (* setoid_ring plugin *)
+| "Add" "Field" ident ":" term1_extended field_mods_opt      (* setoid_ring plugin *)
 | "Print" "Fields"      (* setoid_ring plugin *)
-| "Prenex" "Implicits" global_list      (* ssr plugin *)
-| "Search" ssr_search_arg ssr_modlocs      (* ssr plugin *)
-| "Print" "Hint" "View" ssrviewpos      (* ssr plugin *)
-| "Hint" "View" ssrviewposspc ssrhintref_list      (* ssr plugin *)
+| "Numeral" "Notation" qualid qualid qualid ":" ident numnotoption
+| "String" "Notation" qualid qualid qualid ":" ident
 ]
 
-comment_list_opt: [
-| comment_list_opt comment
+orient: [
+| "->"
+| "<-"
 | empty
 ]
 
-Verbose_opt: [
-| "Verbose"
+string_opt: [
+| string
 | empty
 ]
 
-ne_string_alt: [
-| ne_string
-| IDENT
+qualid_list_opt: [
+| qualid_list_opt qualid
+| empty
 ]
 
-ne_string_list: [
-| ne_string_list ne_string
-| ne_string
+univ_name_list_opt: [
+| "@{" name_list_opt "}"
+| empty
 ]
 
-univ_name_list_opt: [
-| univ_name_list
+name_list_opt: [
+| name_list_opt name
 | empty
 ]
 
-option_ref_value_list: [
-| option_ref_value_list option_ref_value
-| option_ref_value
+section_subset_expr: [
+| starredidentref_list_opt
+| ssexpr
 ]
 
-discriminated_opt: [
-| "discriminated"
-| empty
+ssexpr: [
+| "-" ssexpr50
+| ssexpr50
 ]
 
-global_list: [
-| global_list global
-| global
+ssexpr50: [
+| ssexpr0 "-" ssexpr0
+| ssexpr0 "+" ssexpr0
+| ssexpr0
 ]
 
-preident_list_opt: [
-| preident_list_opt preident
-| empty
+ssexpr0: [
+| starredidentref
+| "(" starredidentref_list_opt ")"
+| "(" starredidentref_list_opt ")" "*"
+| "(" ssexpr ")"
+| "(" ssexpr ")" "*"
 ]
 
-reference_list_opt: [
-| reference_list_opt reference
+starredidentref_list_opt: [
+| starredidentref_list_opt starredidentref
 | empty
 ]
 
+starredidentref: [
+| ident
+| ident "*"
+| "Type"
+| "Type" "*"
+]
+
 int_opt: [
 | int
 | empty
@@ -1580,12 +1532,12 @@ using_opt: [
 ]
 
 with_opt: [
-| "with" tactic
+| "with" ltac_expr
 | empty
 ]
 
 ltac_tactic_level_opt: [
-| ltac_tactic_level
+| "(" "at" "level" num ")"
 | empty
 ]
 
@@ -1594,85 +1546,17 @@ ltac_production_item_list: [
 | ltac_production_item
 ]
 
-ltac_tacdef_body_list: [
-| ltac_tacdef_body_list "with" ltac_tacdef_body
-| ltac_tacdef_body
-]
-
-int_or_id_list_opt: [
-| int_or_id_list_opt int_or_id
-| empty
-]
-
-ident_list: [
-| ident_list ident
-| ident
-]
-
-string_list_opt: [
-| string_list_opt string
-| empty
-]
-
-mlname_list_opt: [
-| mlname_list_opt mlname
-| empty
-]
-
-string_opt: [
-| string
-| empty
-]
-
-function_rec_definition_loc_list: [
-| function_rec_definition_loc_list "with" function_rec_definition_loc
-| function_rec_definition_loc
-]
-
-fun_scheme_arg_list: [
-| fun_scheme_arg_list "with" fun_scheme_arg
-| fun_scheme_arg
-]
-
-ring_mods_opt: [
-| ring_mods
-| empty
-]
-
-field_mods_opt: [
-| field_mods
-| empty
-]
-
-ssrhintref_list: [
-| ssrhintref_list ssrhintref
-| ssrhintref
-]
-
-query_command: [
-| "Eval" red_expr "in" lconstr "."
-| "Compute" lconstr "."
-| "Check" lconstr "."
-| "About" smart_global univ_name_list_opt "."
-| "SearchHead" constr_pattern in_or_out_modules "."
-| "SearchPattern" constr_pattern in_or_out_modules "."
-| "SearchRewrite" constr_pattern in_or_out_modules "."
-| "Search" searchabout_query searchabout_queries "."
-| "SearchAbout" searchabout_query searchabout_queries "."
-| "SearchAbout" "[" searchabout_query_list "]" in_or_out_modules "."
-]
-
-searchabout_query_list: [
-| searchabout_query_list searchabout_query
-| searchabout_query
+tacdef_body_list: [
+| tacdef_body_list "with" tacdef_body
+| tacdef_body
 ]
 
 printable: [
 | "Term" smart_global univ_name_list_opt
 | "All"
-| "Section" global
-| "Grammar" IDENT
-| "Custom" "Grammar" IDENT
+| "Section" qualid
+| "Grammar" ident
+| "Custom" "Grammar" ident
 | "LoadPath" dirpath_opt
 | "Modules"
 | "Libraries"
@@ -1686,17 +1570,18 @@ printable: [
 | "Coercions"
 | "Coercion" "Paths" class_rawexpr class_rawexpr
 | "Canonical" "Projections"
+| "Typing" "Flags"
 | "Tables"
 | "Options"
 | "Hint"
 | "Hint" smart_global
 | "Hint" "*"
-| "HintDb" IDENT
+| "HintDb" ident
 | "Scopes"
-| "Scope" IDENT
-| "Visibility" IDENT_opt3
+| "Scope" ident
+| "Visibility" ident_opt
 | "Implicit" smart_global
-| Sorted_opt "Universes" printunivs_subgraph_opt ne_string_opt
+| Sorted_opt "Universes" printunivs_subgraph_opt string_opt
 | "Assumptions" smart_global
 | "Opaque" "Dependencies" smart_global
 | "Transparent" "Dependencies" smart_global
@@ -1711,9 +1596,9 @@ dirpath_opt: [
 | empty
 ]
 
-IDENT_opt3: [
-| IDENT
-| empty
+dirpath: [
+| ident
+| dirpath field
 ]
 
 Sorted_opt: [
@@ -1722,384 +1607,408 @@ Sorted_opt: [
 ]
 
 printunivs_subgraph_opt: [
-| printunivs_subgraph
+| "Subgraph" "(" qualid_list_opt ")"
 | empty
 ]
 
-ne_string_opt: [
-| ne_string
+comment_list_opt: [
+| comment_list_opt comment
 | empty
 ]
 
-printunivs_subgraph: [
-| "Subgraph" "(" reference_list_opt ")"
+Verbose_opt: [
+| "Verbose"
+| empty
 ]
 
-class_rawexpr: [
-| "Funclass"
-| "Sortclass"
-| smart_global
+string_alt: [
+| string
+| ident
 ]
 
-locatable: [
-| smart_global
-| "Term" smart_global
-| "File" ne_string
-| "Library" global
-| "Module" global
+string_list: [
+| string_list string
+| string
 ]
 
-option_setting: [
-| empty
-| integer
-| STRING
+option_ref_value_list: [
+| option_ref_value_list option_ref_value
+| option_ref_value
 ]
 
-option_ref_value: [
-| global
-| STRING
+discriminated_opt: [
+| "discriminated"
+| empty
 ]
 
-option_table: [
-| IDENT_list
+string_list_opt: [
+| string_list_opt string
+| empty
 ]
 
-as_dirpath: [
-| as_opt3
+mlname_list_opt: [
+| mlname_list_opt mlname
+| empty
 ]
 
-as_opt: [
-| "as" name
-| empty
+fun_scheme_arg_list: [
+| fun_scheme_arg_list "with" fun_scheme_arg
+| fun_scheme_arg
 ]
 
-ne_in_or_out_modules: [
-| "inside" global_list
-| "outside" global_list
+term1_extended_list: [
+| term1_extended_list term1_extended
+| term1_extended
 ]
 
-in_or_out_modules: [
-| ne_in_or_out_modules
+ring_mods_opt: [
+| "(" ring_mod_list_comma ")"      (* setoid_ring plugin *)
 | empty
 ]
 
-comment: [
-| term
-| STRING
-| natural
+field_mods_opt: [
+| "(" field_mod_list_comma ")"      (* setoid_ring plugin *)
+| empty
 ]
 
-positive_search_mark: [
-| "-"
-| empty
+locatable: [
+| smart_global
+| "Term" smart_global
+| "File" string
+| "Library" qualid
+| "Module" qualid
 ]
 
-searchabout_query: [
-| positive_search_mark ne_string scope_opt
-| positive_search_mark constr_pattern
+option_ref_value: [
+| qualid
+| string
 ]
 
-searchabout_queries: [
-| ne_in_or_out_modules
-| searchabout_query searchabout_queries
+as_dirpath: [
+| "as" dirpath
 | empty
 ]
 
-univ_name_list: [
-| "@{" name_list_opt "}"
+comment: [
+| term1_extended
+| string
+| num
 ]
 
-syntax: [
-| "Open" "Scope" IDENT
-| "Close" "Scope" IDENT
-| "Delimit" "Scope" IDENT; "with" IDENT
-| "Undelimit" "Scope" IDENT
-| "Bind" "Scope" IDENT; "with" class_rawexpr_list
-| "Infix" ne_lstring ":=" term syntax_modifier_opt IDENT_opt2
-| "Notation" ident ident_list_opt ":=" term only_parsing
-| "Notation" lstring ":=" term syntax_modifier_opt IDENT_opt2
-| "Format" "Notation" STRING STRING STRING
-| "Reserved" "Infix" ne_lstring syntax_modifier_opt
-| "Reserved" "Notation" ne_lstring syntax_modifier_opt
+reference_or_constr: [
+| qualid
+| term1_extended
 ]
 
-class_rawexpr_list: [
-| class_rawexpr_list class_rawexpr
-| class_rawexpr
+hint: [
+| "Resolve" reference_or_constr_list hint_info
+| "Resolve" "->" qualid_list num_opt
+| "Resolve" "<-" qualid_list num_opt
+| "Immediate" reference_or_constr_list
+| "Variables" "Transparent"
+| "Variables" "Opaque"
+| "Constants" "Transparent"
+| "Constants" "Opaque"
+| "Transparent" qualid_list
+| "Opaque" qualid_list
+| "Mode" qualid plus_list
+| "Unfold" qualid_list
+| "Constructors" qualid_list
+| "Extern" num term1_extended_opt "=>" ltac_expr
 ]
 
-syntax_modifier_opt: [
-| "(" syntax_modifier_list_comma ")"
-| empty
+reference_or_constr_list: [
+| reference_or_constr_list reference_or_constr
+| reference_or_constr
 ]
 
-syntax_modifier_list_comma: [
-| syntax_modifier_list_comma "," syntax_modifier
-| syntax_modifier
+constr_body: [
+| ":=" term
+| ":" term ":=" term
 ]
 
-only_parsing: [
-| "(" "only" "parsing" ")"
-| "(" "compat" STRING ")"
-| empty
+plus_list: [
+| plus_list plus_alt
+| plus_alt
 ]
 
-level: [
-| "level" natural
-| "next" "level"
+plus_alt: [
+| "+"
+| "!"
+| "-"
 ]
 
-syntax_modifier: [
-| "at" "level" natural
-| "in" "custom" IDENT
-| "in" "custom" IDENT; "at" "level" natural
-| "left" "associativity"
-| "right" "associativity"
-| "no" "associativity"
-| "only" "printing"
-| "only" "parsing"
-| "compat" STRING
-| "format" STRING STRING_opt
-| IDENT; "," IDENT_list_comma "at" level
-| IDENT; "at" level
-| IDENT; "at" level constr_as_binder_kind
-| IDENT constr_as_binder_kind
-| IDENT syntax_extension_type
+withtac: [
+| "with" ltac_expr
+| empty
 ]
 
-STRING_opt: [
-| STRING
-| empty
+ltac_def_kind: [
+| ":="
+| "::="
 ]
 
-IDENT_list_comma: [
-| IDENT_list_comma "," IDENT
-| IDENT
+tacdef_body: [
+| qualid fun_var_list ltac_def_kind ltac_expr
+| qualid ltac_def_kind ltac_expr
 ]
 
-syntax_extension_type: [
-| "ident"
-| "global"
-| "bigint"
-| "binder"
-| "constr"
-| "constr" at_level_opt constr_as_binder_kind_opt
-| "pattern"
-| "pattern" "at" "level" natural
-| "strict" "pattern"
-| "strict" "pattern" "at" "level" natural
-| "closed" "binder"
-| "custom" IDENT at_level_opt constr_as_binder_kind_opt
+ltac_production_item: [
+| string
+| ident "(" ident ltac_production_sep_opt ")"
+| ident
 ]
 
-at_level_opt: [
-| at_level
+ltac_production_sep_opt: [
+| "," string
 | empty
 ]
 
-constr_as_binder_kind_opt: [
-| constr_as_binder_kind
+numnotoption: [
 | empty
+| "(" "warning" "after" num ")"
+| "(" "abstract" "after" num ")"
 ]
 
-at_level: [
-| "at" level
+mlname: [
+| ident      (* extraction plugin *)
+| string      (* extraction plugin *)
 ]
 
-constr_as_binder_kind: [
-| "as" "ident"
-| "as" "pattern"
-| "as" "strict" "pattern"
+int_or_id: [
+| ident      (* extraction plugin *)
+| int      (* extraction plugin *)
 ]
 
-opt_hintbases: [
-| empty
-| ":" IDENT_list
+language: [
+| "Ocaml"      (* extraction plugin *)
+| "OCaml"      (* extraction plugin *)
+| "Haskell"      (* extraction plugin *)
+| "Scheme"      (* extraction plugin *)
+| "JSON"      (* extraction plugin *)
 ]
 
-IDENT_list: [
-| IDENT_list IDENT
-| IDENT
+fun_scheme_arg: [
+| ident ":=" "Induction" "for" qualid "Sort" sort_family      (* funind plugin *)
 ]
 
-reference_or_constr: [
-| global
-| term
+ring_mod: [
+| "decidable" term1_extended      (* setoid_ring plugin *)
+| "abstract"      (* setoid_ring plugin *)
+| "morphism" term1_extended      (* setoid_ring plugin *)
+| "constants" "[" ltac_expr "]"      (* setoid_ring plugin *)
+| "closed" "[" qualid_list "]"      (* setoid_ring plugin *)
+| "preprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
+| "postprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
+| "setoid" term1_extended term1_extended      (* setoid_ring plugin *)
+| "sign" term1_extended      (* setoid_ring plugin *)
+| "power" term1_extended "[" qualid_list "]"      (* setoid_ring plugin *)
+| "power_tac" term1_extended "[" ltac_expr "]"      (* setoid_ring plugin *)
+| "div" term1_extended      (* setoid_ring plugin *)
 ]
 
-hint: [
-| "Resolve" reference_or_constr_list hint_info
-| "Resolve" "->" global_list natural_opt
-| "Resolve" "<-" global_list natural_opt
-| "Immediate" reference_or_constr_list
-| "Variables" "Transparent"
-| "Variables" "Opaque"
-| "Constants" "Transparent"
-| "Constants" "Opaque"
-| "Transparent" global_list
-| "Opaque" global_list
-| "Mode" global mode
-| "Unfold" global_list
-| "Constructors" global_list
-| "Extern" natural constr_pattern_opt "=>" tactic
+ring_mod_list_comma: [
+| ring_mod_list_comma "," ring_mod
+| ring_mod
 ]
 
-reference_or_constr_list: [
-| reference_or_constr_list reference_or_constr
-| reference_or_constr
+field_mod: [
+| ring_mod      (* setoid_ring plugin *)
+| "completeness" term1_extended      (* setoid_ring plugin *)
 ]
 
-natural_opt2: [
-| "|" natural
-| empty
+field_mod_list_comma: [
+| field_mod_list_comma "," field_mod
+| field_mod
 ]
 
-constr_pattern_opt: [
-| constr_pattern
+debug: [
+| "debug"
 | empty
 ]
 
-constr_body: [
-| ":=" lconstr
-| ":" lconstr ":=" lconstr
+eauto_search_strategy: [
+| "(bfs)"
+| "(dfs)"
+| empty
 ]
 
-mode: [
-| plus_list
+hints_path_atom: [
+| qualid_list
+| "_"
 ]
 
-plus_list: [
-| plus_list plus_alt
-| plus_alt
+hints_path: [
+| "(" hints_path ")"
+| hints_path "*"
+| "emp"
+| "eps"
+| hints_path "|" hints_path
+| hints_path_atom
+| hints_path hints_path
 ]
 
-plus_alt: [
-| "+"
-| "!"
-| "-"
+opthints: [
+| ":" ident_list
+| empty
 ]
 
-vernac_toplevel: [
-| "Drop" "."
-| "Quit" "."
-| "Backtrack" natural natural natural "."
-| "Show" "Goal" natural "at" natural "."
-| vernac_control
+opt_hintbases: [
+| empty
+| ":" ident_list
 ]
 
-orient: [
-| "->"
-| "<-"
+int_or_id_list_opt: [
+| int_or_id_list_opt int_or_id
 | empty
 ]
 
-occurrences: [
-| integer_list
-| var
+query_command: [
+| "Eval" red_expr "in" term "."
+| "Compute" term "."
+| "Check" term "."
+| "About" smart_global univ_name_list_opt "."
+| "SearchHead" term1_extended in_or_out_modules "."
+| "SearchPattern" term1_extended in_or_out_modules "."
+| "SearchRewrite" term1_extended in_or_out_modules "."
+| "Search" searchabout_query searchabout_queries "."
+| "SearchAbout" searchabout_query searchabout_queries "."
+| "SearchAbout" "[" searchabout_query_list "]" in_or_out_modules "."
 ]
 
-integer_list: [
-| integer_list integer
-| integer
+ne_in_or_out_modules: [
+| "inside" qualid_list
+| "outside" qualid_list
 ]
 
-glob: [
-| term
+in_or_out_modules: [
+| ne_in_or_out_modules
+| empty
 ]
 
-lglob: [
-| lconstr
+positive_search_mark: [
+| "-"
+| empty
 ]
 
-casted_constr: [
-| term
+searchabout_query: [
+| positive_search_mark string scope_delimiter_opt
+| positive_search_mark term1_extended
 ]
 
-hloc: [
+searchabout_queries: [
+| ne_in_or_out_modules
+| searchabout_query searchabout_queries
 | empty
-| "in" "|-" "*"
-| "in" ident
-| "in" "(" "Type" "of" ident ")"
-| "in" "(" "Value" "of" ident ")"
-| "in" "(" "type" "of" ident ")"
-| "in" "(" "value" "of" ident ")"
 ]
 
-rename: [
-| ident "into" ident
+searchabout_query_list: [
+| searchabout_query_list searchabout_query
+| searchabout_query
 ]
 
-by_arg_tac: [
-| "by" ltac_expr3
-| empty
+syntax: [
+| "Open" "Scope" ident
+| "Close" "Scope" ident
+| "Delimit" "Scope" ident "with" ident
+| "Undelimit" "Scope" ident
+| "Bind" "Scope" ident "with" class_rawexpr_list
+| "Infix" string ":=" term1_extended syntax_modifier_opt ident_opt3
+| "Notation" ident ident_list_opt ":=" term1_extended only_parsing
+| "Notation" string ":=" term1_extended syntax_modifier_opt ident_opt3
+| "Format" "Notation" string string string
+| "Reserved" "Infix" string syntax_modifier_opt
+| "Reserved" "Notation" string syntax_modifier_opt
 ]
 
-in_clause: [
-| in_clause
-| "*" occs
-| "*" "|-" concl_occ
-| hypident_occ_list_comma_opt "|-" concl_occ
-| hypident_occ_list_comma_opt
+class_rawexpr_list: [
+| class_rawexpr_list class_rawexpr
+| class_rawexpr
 ]
 
-hypident_occ_list_comma_opt: [
-| hypident_occ_list_comma
+syntax_modifier_opt: [
+| "(" syntax_modifier_list_comma ")"
 | empty
 ]
 
-hypident_occ_list_comma: [
-| hypident_occ_list_comma "," hypident_occ
-| hypident_occ
+syntax_modifier_list_comma: [
+| syntax_modifier_list_comma "," syntax_modifier
+| syntax_modifier
 ]
 
-test_lpar_id_colon: [
+only_parsing: [
+| "(" "only" "parsing" ")"
+| "(" "compat" string ")"
 | empty
 ]
 
-withtac: [
-| "with" tactic
-| empty
+level: [
+| "level" num
+| "next" "level"
 ]
 
-closed_binder: [
-| "(" name name_list ":" lconstr ")"
-| "(" name ":" lconstr ")"
-| "(" name ":=" lconstr ")"
-| "(" name ":" lconstr ":=" lconstr ")"
-| "{" name "}"
-| "{" name name_list ":" lconstr "}"
-| "{" name ":" lconstr "}"
-| "{" name name_list "}"
-| "`(" typeclass_constraint_list_comma ")"
-| "`{" typeclass_constraint_list_comma "}"
-| "'" pattern0
-| of_alt operconstr99      (* ssr plugin *)
-| "(" "_" ":" lconstr "|" lconstr ")"
+syntax_modifier: [
+| "at" "level" num
+| "in" "custom" ident
+| "in" "custom" ident "at" "level" num
+| "left" "associativity"
+| "right" "associativity"
+| "no" "associativity"
+| "only" "printing"
+| "only" "parsing"
+| "compat" string
+| "format" string string_opt
+| ident "," ident_list_comma "at" level
+| ident "at" level
+| ident "at" level constr_as_binder_kind
+| ident constr_as_binder_kind
+| ident syntax_extension_type
 ]
 
-typeclass_constraint_list_comma: [
-| typeclass_constraint_list_comma "," typeclass_constraint
-| typeclass_constraint
+syntax_extension_type: [
+| "ident"
+| "global"
+| "bigint"
+| "binder"
+| "constr"
+| "constr" level_opt constr_as_binder_kind_opt
+| "pattern"
+| "pattern" "at" "level" num
+| "strict" "pattern"
+| "strict" "pattern" "at" "level" num
+| "closed" "binder"
+| "custom" ident level_opt constr_as_binder_kind_opt
 ]
 
-of_alt: [
-| "of"
-| "&"
+level_opt: [
+| level
+| empty
+]
+
+constr_as_binder_kind_opt: [
+| constr_as_binder_kind
+| empty
+]
+
+constr_as_binder_kind: [
+| "as" "ident"
+| "as" "pattern"
+| "as" "strict" "pattern"
 ]
 
 simple_tactic: [
 | "reflexivity"
-| "exact" casted_constr
+| "exact" term1_extended
 | "assumption"
 | "etransitivity"
-| "cut" term
-| "exact_no_check" term
-| "vm_cast_no_check" term
-| "native_cast_no_check" term
-| "casetype" term
-| "elimtype" term
-| "lapply" term
-| "transitivity" term
+| "cut" term1_extended
+| "exact_no_check" term1_extended
+| "vm_cast_no_check" term1_extended
+| "native_cast_no_check" term1_extended
+| "casetype" term1_extended
+| "elimtype" term1_extended
+| "lapply" term1_extended
+| "transitivity" term1_extended
 | "left"
 | "eleft"
 | "left" "with" bindings
@@ -2131,32 +2040,32 @@ simple_tactic: [
 | "intro" ident
 | "intro" ident "at" "top"
 | "intro" ident "at" "bottom"
-| "intro" ident "after" var
-| "intro" ident "before" var
+| "intro" ident "after" ident
+| "intro" ident "before" ident
 | "intro" "at" "top"
 | "intro" "at" "bottom"
-| "intro" "after" var
-| "intro" "before" var
-| "move" var "at" "top"
-| "move" var "at" "bottom"
-| "move" var "after" var
-| "move" var "before" var
+| "intro" "after" ident
+| "intro" "before" ident
+| "move" ident "at" "top"
+| "move" ident "at" "bottom"
+| "move" ident "after" ident
+| "move" ident "before" ident
 | "rename" rename_list_comma
-| "revert" var_list
+| "revert" ident_list
 | "simple" "induction" quantified_hypothesis
 | "simple" "destruct" quantified_hypothesis
 | "double" "induction" quantified_hypothesis quantified_hypothesis
 | "admit"
-| "fix" ident natural
+| "fix" ident num
 | "cofix" ident
-| "clear" var_list_opt
-| "clear" "-" var_list
-| "clearbody" var_list
-| "generalize" "dependent" term
-| "replace" uconstr "with" term clause_dft_concl by_arg_tac
-| "replace" "->" uconstr clause_dft_concl
-| "replace" "<-" uconstr clause_dft_concl
-| "replace" uconstr clause_dft_concl
+| "clear" ident_list_opt
+| "clear" "-" ident_list
+| "clearbody" ident_list
+| "generalize" "dependent" term1_extended
+| "replace" term1_extended "with" term1_extended clause_dft_concl by_arg_tac
+| "replace" "->" term1_extended clause_dft_concl
+| "replace" "<-" term1_extended clause_dft_concl
+| "replace" term1_extended clause_dft_concl
 | "simplify_eq"
 | "simplify_eq" destruction_arg
 | "esimplify_eq"
@@ -2175,64 +2084,64 @@ simple_tactic: [
 | "einjection" destruction_arg "as" simple_intropattern_list_opt
 | "simple" "injection"
 | "simple" "injection" destruction_arg
-| "dependent" "rewrite" orient term
-| "dependent" "rewrite" orient term "in" var
-| "cutrewrite" orient term
-| "cutrewrite" orient term "in" var
-| "decompose" "sum" term
-| "decompose" "record" term
-| "absurd" term
+| "dependent" "rewrite" orient term1_extended
+| "dependent" "rewrite" orient term1_extended "in" ident
+| "cutrewrite" orient term1_extended
+| "cutrewrite" orient term1_extended "in" ident
+| "decompose" "sum" term1_extended
+| "decompose" "record" term1_extended
+| "absurd" term1_extended
 | "contradiction" constr_with_bindings_opt
-| "autorewrite" "with" preident_list clause_dft_concl
-| "autorewrite" "with" preident_list clause_dft_concl "using" tactic
-| "autorewrite" "*" "with" preident_list clause_dft_concl
-| "autorewrite" "*" "with" preident_list clause_dft_concl "using" tactic
-| "rewrite" "*" orient uconstr "in" var "at" occurrences by_arg_tac
-| "rewrite" "*" orient uconstr "at" occurrences "in" var by_arg_tac
-| "rewrite" "*" orient uconstr "in" var by_arg_tac
-| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac
-| "rewrite" "*" orient uconstr by_arg_tac
-| "refine" uconstr
-| "simple" "refine" uconstr
-| "notypeclasses" "refine" uconstr
-| "simple" "notypeclasses" "refine" uconstr
+| "autorewrite" "with" ident_list clause_dft_concl
+| "autorewrite" "with" ident_list clause_dft_concl "using" ltac_expr
+| "autorewrite" "*" "with" ident_list clause_dft_concl
+| "autorewrite" "*" "with" ident_list clause_dft_concl "using" ltac_expr
+| "rewrite" "*" orient term1_extended "in" ident "at" occurrences by_arg_tac
+| "rewrite" "*" orient term1_extended "at" occurrences "in" ident by_arg_tac
+| "rewrite" "*" orient term1_extended "in" ident by_arg_tac
+| "rewrite" "*" orient term1_extended "at" occurrences by_arg_tac
+| "rewrite" "*" orient term1_extended by_arg_tac
+| "refine" term1_extended
+| "simple" "refine" term1_extended
+| "notypeclasses" "refine" term1_extended
+| "simple" "notypeclasses" "refine" term1_extended
 | "solve_constraints"
-| "subst" var_list
+| "subst" ident_list
 | "subst"
 | "simple" "subst"
-| "evar" test_lpar_id_colon "(" ident ":" lconstr ")"
-| "evar" term
-| "instantiate" "(" ident ":=" lglob ")"
-| "instantiate" "(" integer ":=" lglob ")" hloc
+| "evar" "(" ident ":" term ")"
+| "evar" term1_extended
+| "instantiate" "(" ident ":=" term ")"
+| "instantiate" "(" int ":=" term ")" hloc
 | "instantiate"
-| "stepl" term "by" tactic
-| "stepl" term
-| "stepr" term "by" tactic
-| "stepr" term
-| "generalize_eqs" var
-| "dependent" "generalize_eqs" var
-| "generalize_eqs_vars" var
-| "dependent" "generalize_eqs_vars" var
-| "specialize_eqs" var
-| "hresolve_core" "(" ident ":=" term ")" "at" int_or_var "in" term
-| "hresolve_core" "(" ident ":=" term ")" "in" term
+| "stepl" term1_extended "by" ltac_expr
+| "stepl" term1_extended
+| "stepr" term1_extended "by" ltac_expr
+| "stepr" term1_extended
+| "generalize_eqs" ident
+| "dependent" "generalize_eqs" ident
+| "generalize_eqs_vars" ident
+| "dependent" "generalize_eqs_vars" ident
+| "specialize_eqs" ident
+| "hresolve_core" "(" ident ":=" term1_extended ")" "at" int_or_var "in" term1_extended
+| "hresolve_core" "(" ident ":=" term1_extended ")" "in" term1_extended
 | "hget_evar" int_or_var
 | "destauto"
-| "destauto" "in" var
+| "destauto" "in" ident
 | "transparent_abstract" ltac_expr3
 | "transparent_abstract" ltac_expr3 "using" ident
-| "constr_eq" term term
-| "constr_eq_strict" term term
-| "constr_eq_nounivs" term term
-| "is_evar" term
-| "has_evar" term
-| "is_var" term
-| "is_fix" term
-| "is_cofix" term
-| "is_ind" term
-| "is_constructor" term
-| "is_proj" term
-| "is_const" term
+| "constr_eq" term1_extended term1_extended
+| "constr_eq_strict" term1_extended term1_extended
+| "constr_eq_nounivs" term1_extended term1_extended
+| "is_evar" term1_extended
+| "has_evar" term1_extended
+| "is_var" term1_extended
+| "is_fix" term1_extended
+| "is_cofix" term1_extended
+| "is_ind" term1_extended
+| "is_constructor" term1_extended
+| "is_proj" term1_extended
+| "is_const" term1_extended
 | "shelve"
 | "shelve_unifiable"
 | "unshelve" ltac_expr1
@@ -2240,8 +2149,8 @@ simple_tactic: [
 | "cycle" int_or_var
 | "swap" int_or_var int_or_var
 | "revgoals"
-| "guard" test
-| "decompose" "[" term_list "]" term
+| "guard" int_or_var comparison int_or_var
+| "decompose" "[" term1_extended_list "]" term1_extended
 | "optimize_heap"
 | "start" "ltac" "profiling"
 | "stop" "ltac" "profiling"
@@ -2253,51 +2162,51 @@ simple_tactic: [
 | "finish_timing" string_opt
 | "finish_timing" "(" string ")" string_opt
 | "eassumption"
-| "eexact" term
+| "eexact" term1_extended
 | "trivial" auto_using hintbases
 | "info_trivial" auto_using hintbases
 | "debug" "trivial" auto_using hintbases
 | "auto" int_or_var_opt auto_using hintbases
 | "info_auto" int_or_var_opt auto_using hintbases
 | "debug" "auto" int_or_var_opt auto_using hintbases
-| "prolog" "[" uconstr_list_opt "]" int_or_var
+| "prolog" "[" term1_extended_list_opt "]" int_or_var
 | "eauto" int_or_var_opt int_or_var_opt auto_using hintbases
 | "new" "auto" int_or_var_opt auto_using hintbases
 | "debug" "eauto" int_or_var_opt int_or_var_opt auto_using hintbases
 | "info_eauto" int_or_var_opt int_or_var_opt auto_using hintbases
 | "dfs" "eauto" int_or_var_opt auto_using hintbases
 | "autounfold" hintbases clause_dft_concl
-| "autounfold_one" hintbases "in" var
+| "autounfold_one" hintbases "in" ident
 | "autounfold_one" hintbases
-| "unify" term term
-| "unify" term term "with" preident
-| "convert_concl_no_check" term
-| "typeclasses" "eauto" "bfs" int_or_var_opt "with" preident_list
-| "typeclasses" "eauto" int_or_var_opt "with" preident_list
+| "unify" term1_extended term1_extended
+| "unify" term1_extended term1_extended "with" ident
+| "convert_concl_no_check" term1_extended
+| "typeclasses" "eauto" "bfs" int_or_var_opt "with" ident_list
+| "typeclasses" "eauto" int_or_var_opt "with" ident_list
 | "typeclasses" "eauto" int_or_var_opt
-| "head_of_constr" ident term
-| "not_evar" term
-| "is_ground" term
-| "autoapply" term "using" preident
-| "autoapply" term "with" preident
-| "progress_evars" tactic
-| "rewrite_strat" rewstrategy "in" var
+| "head_of_constr" ident term1_extended
+| "not_evar" term1_extended
+| "is_ground" term1_extended
+| "autoapply" term1_extended "using" ident
+| "autoapply" term1_extended "with" ident
+| "progress_evars" ltac_expr
 | "rewrite_strat" rewstrategy
-| "rewrite_db" preident "in" var
-| "rewrite_db" preident
-| "substitute" orient glob_constr_with_bindings
-| "setoid_rewrite" orient glob_constr_with_bindings
-| "setoid_rewrite" orient glob_constr_with_bindings "in" var
-| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences
-| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" var
-| "setoid_rewrite" orient glob_constr_with_bindings "in" var "at" occurrences
+| "rewrite_db" ident "in" ident
+| "rewrite_db" ident
+| "substitute" orient constr_with_bindings
+| "setoid_rewrite" orient constr_with_bindings
+| "setoid_rewrite" orient constr_with_bindings "in" ident
+| "setoid_rewrite" orient constr_with_bindings "at" occurrences
+| "setoid_rewrite" orient constr_with_bindings "at" occurrences "in" ident
+| "setoid_rewrite" orient constr_with_bindings "in" ident "at" occurrences
 | "setoid_symmetry"
-| "setoid_symmetry" "in" var
+| "setoid_symmetry" "in" ident
 | "setoid_reflexivity"
-| "setoid_transitivity" term
+| "setoid_transitivity" term1_extended
 | "setoid_etransitivity"
 | "decide" "equality"
-| "compare" term term
+| "compare" term1_extended term1_extended
+| "rewrite_strat" rewstrategy "in" ident
 | "intros" intropattern_list_opt
 | "eintros" intropattern_list_opt
 | "apply" constr_with_bindings_arg_list_comma in_hyp_as
@@ -2308,33 +2217,33 @@ simple_tactic: [
 | "eelim" constr_with_bindings_arg eliminator_opt
 | "case" induction_clause_list
 | "ecase" induction_clause_list
-| "fix" ident natural "with" fixdecl_list
+| "fix" ident num "with" fixdecl_list
 | "cofix" ident "with" cofixdecl_list
 | "pose" bindings_with_parameters
-| "pose" term as_name
+| "pose" term1_extended as_name
 | "epose" bindings_with_parameters
-| "epose" term as_name
+| "epose" term1_extended as_name
 | "set" bindings_with_parameters clause_dft_concl
-| "set" term as_name clause_dft_concl
+| "set" term1_extended as_name clause_dft_concl
 | "eset" bindings_with_parameters clause_dft_concl
-| "eset" term as_name clause_dft_concl
-| "remember" term as_name eqn_ipat clause_dft_all
-| "eremember" term as_name eqn_ipat clause_dft_all
-| "assert" "(" ident ":=" lconstr ")"
-| "eassert" "(" ident ":=" lconstr ")"
-| "assert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic
-| "eassert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic
-| "enough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic
-| "eenough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic
-| "assert" term as_ipat by_tactic
-| "eassert" term as_ipat by_tactic
-| "pose" "proof" lconstr as_ipat
-| "epose" "proof" lconstr as_ipat
-| "enough" term as_ipat by_tactic
-| "eenough" term as_ipat by_tactic
-| "generalize" term
-| "generalize" term term_list
-| "generalize" term occs as_name pattern_occ_list_opt
+| "eset" term1_extended as_name clause_dft_concl
+| "remember" term1_extended as_name eqn_ipat clause_dft_all
+| "eremember" term1_extended as_name eqn_ipat clause_dft_all
+| "assert" "(" ident ":=" term ")"
+| "eassert" "(" ident ":=" term ")"
+| "assert" "(" ident ":" term ")" by_tactic
+| "eassert" "(" ident ":" term ")" by_tactic
+| "enough" "(" ident ":" term ")" by_tactic
+| "eenough" "(" ident ":" term ")" by_tactic
+| "assert" term1_extended as_ipat by_tactic
+| "eassert" term1_extended as_ipat by_tactic
+| "pose" "proof" term as_ipat
+| "epose" "proof" term as_ipat
+| "enough" term1_extended as_ipat by_tactic
+| "eenough" term1_extended as_ipat by_tactic
+| "generalize" term1_extended
+| "generalize" term1_extended term1_extended_list
+| "generalize" term1_extended occs as_name pattern_occ_list_opt
 | "induction" induction_clause_list
 | "einduction" induction_clause_list
 | "destruct" induction_clause_list
@@ -2345,7 +2254,7 @@ simple_tactic: [
 | "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
 | "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
 | "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list
-| "inversion" quantified_hypothesis "using" term in_hyp_list
+| "inversion" quantified_hypothesis "using" term1_extended in_hyp_list
 | "red" clause_dft_concl
 | "hnf" clause_dft_concl
 | "simpl" delta_flag ref_or_pattern_occ_opt clause_dft_concl
@@ -2356,357 +2265,176 @@ simple_tactic: [
 | "vm_compute" ref_or_pattern_occ_opt clause_dft_concl
 | "native_compute" ref_or_pattern_occ_opt clause_dft_concl
 | "unfold" unfold_occ_list_comma clause_dft_concl
-| "fold" term_list clause_dft_concl
+| "fold" term1_extended_list clause_dft_concl
 | "pattern" pattern_occ_list_comma clause_dft_concl
 | "change" conversion clause_dft_concl
 | "change_no_check" conversion clause_dft_concl
 | "btauto"
 | "rtauto"
 | "congruence"
-| "congruence" integer
-| "congruence" "with" term_list
-| "congruence" integer "with" term_list
+| "congruence" int
+| "congruence" "with" term1_extended_list
+| "congruence" int "with" term1_extended_list
 | "f_equal"
-| "firstorder" tactic_opt firstorder_using
-| "firstorder" tactic_opt "with" preident_list
-| "firstorder" tactic_opt firstorder_using "with" preident_list
-| "gintuition" tactic_opt
-| "functional" "inversion" quantified_hypothesis reference_opt      (* funind plugin *)
-| "functional" "induction" term_list fun_ind_using with_names      (* funind plugin *)
-| "soft" "functional" "induction" term_list fun_ind_using with_names      (* funind plugin *)
+| "firstorder" ltac_expr_opt firstorder_using
+| "firstorder" ltac_expr_opt "with" ident_list
+| "firstorder" ltac_expr_opt firstorder_using "with" ident_list
+| "gintuition" ltac_expr_opt
+| "functional" "inversion" quantified_hypothesis qualid_opt      (* funind plugin *)
+| "functional" "induction" term1_extended_list fun_ind_using with_names      (* funind plugin *)
+| "soft" "functional" "induction" term1_extended_list fun_ind_using with_names      (* funind plugin *)
 | "myred"      (* micromega plugin *)
-| "psatz_Z" int_or_var tactic      (* micromega plugin *)
-| "psatz_Z" tactic      (* micromega plugin *)
-| "xlia" tactic      (* micromega plugin *)
-| "xnlia" tactic      (* micromega plugin *)
-| "xnra" tactic      (* micromega plugin *)
-| "xnqa" tactic      (* micromega plugin *)
-| "sos_Z" tactic      (* micromega plugin *)
-| "sos_Q" tactic      (* micromega plugin *)
-| "sos_R" tactic      (* micromega plugin *)
-| "lra_Q" tactic      (* micromega plugin *)
-| "lra_R" tactic      (* micromega plugin *)
-| "psatz_R" int_or_var tactic      (* micromega plugin *)
-| "psatz_R" tactic      (* micromega plugin *)
-| "psatz_Q" int_or_var tactic      (* micromega plugin *)
-| "psatz_Q" tactic      (* micromega plugin *)
-| "nsatz_compute" term      (* nsatz plugin *)
+| "psatz_Z" int_or_var ltac_expr      (* micromega plugin *)
+| "psatz_Z" ltac_expr      (* micromega plugin *)
+| "xlia" ltac_expr      (* micromega plugin *)
+| "xnlia" ltac_expr      (* micromega plugin *)
+| "xnra" ltac_expr      (* micromega plugin *)
+| "xnqa" ltac_expr      (* micromega plugin *)
+| "sos_Z" ltac_expr      (* micromega plugin *)
+| "sos_Q" ltac_expr      (* micromega plugin *)
+| "sos_R" ltac_expr      (* micromega plugin *)
+| "lra_Q" ltac_expr      (* micromega plugin *)
+| "lra_R" ltac_expr      (* micromega plugin *)
+| "psatz_R" int_or_var ltac_expr      (* micromega plugin *)
+| "psatz_R" ltac_expr      (* micromega plugin *)
+| "psatz_Q" int_or_var ltac_expr      (* micromega plugin *)
+| "psatz_Q" ltac_expr      (* micromega plugin *)
+| "iter_specs" ltac_expr      (* micromega plugin *)
+| "zify_op"      (* micromega plugin *)
+| "saturate"      (* micromega plugin *)
+| "nsatz_compute" term1_extended      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
 | "omega" "with" ident_list      (* omega plugin *)
 | "omega" "with" "*"      (* omega plugin *)
 | "protect_fv" string "in" ident      (* setoid_ring plugin *)
 | "protect_fv" string      (* setoid_ring plugin *)
-| "ring_lookup" ltac_expr0 "[" term_list_opt "]" term_list      (* setoid_ring plugin *)
-| "field_lookup" tactic "[" term_list_opt "]" term_list      (* setoid_ring plugin *)
-| "YouShouldNotTypeThis" ssrintrosarg      (* ssr plugin *)
-| "by" ssrhintarg      (* ssr plugin *)
-| "YouShouldNotTypeThis" "do"      (* ssr plugin *)
-| "YouShouldNotTypeThis" ssrtclarg ssrseqarg      (* ssr plugin *)
-| "clear" natural      (* ssr plugin *)
-| "move" ssrmovearg ssrrpat      (* ssr plugin *)
-| "move" ssrmovearg ssrclauses      (* ssr plugin *)
-| "move" ssrrpat      (* ssr plugin *)
-| "move"      (* ssr plugin *)
-| "case" ssrcasearg ssrclauses      (* ssr plugin *)
-| "case"      (* ssr plugin *)
-| "elim" ssrarg ssrclauses      (* ssr plugin *)
-| "elim"      (* ssr plugin *)
-| "apply" ssrapplyarg      (* ssr plugin *)
-| "apply"      (* ssr plugin *)
-| "exact" ssrexactarg      (* ssr plugin *)
-| "exact"      (* ssr plugin *)
-| "exact" "<:" lconstr      (* ssr plugin *)
-| "congr" ssrcongrarg      (* ssr plugin *)
-| "ssrinstancesofruleL2R" ssrterm      (* ssr plugin *)
-| "ssrinstancesofruleR2L" ssrterm      (* ssr plugin *)
-| "rewrite" ssrrwargs ssrclauses      (* ssr plugin *)
-| "unlock" ssrunlockargs ssrclauses      (* ssr plugin *)
-| "pose" ssrfixfwd      (* ssr plugin *)
-| "pose" ssrcofixfwd      (* ssr plugin *)
-| "pose" ssrfwdid ssrposefwd      (* ssr plugin *)
-| "set" ssrfwdid ssrsetfwd ssrclauses      (* ssr plugin *)
-| "abstract" ssrdgens      (* ssr plugin *)
-| "have" ssrhavefwdwbinders      (* ssr plugin *)
-| "have" "suff" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
-| "have" "suffices" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
-| "suff" "have" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
-| "suffices" "have" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
-| "suff" ssrsufffwd      (* ssr plugin *)
-| "suffices" ssrsufffwd      (* ssr plugin *)
-| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
-| "under" ssrrwarg      (* ssr plugin *)
-| "under" ssrrwarg ssrintros_ne      (* ssr plugin *)
-| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg      (* ssr plugin *)
-| "under" ssrrwarg "do" ssrhint3arg      (* ssr plugin *)
-| "ssrinstancesoftpat" cpattern      (* ssrmatching plugin *)
-]
-
-var_list: [
-| var_list var
-| var
-]
-
-var_list_opt: [
-| var_list_opt var
-| empty
+| "ring_lookup" ltac_expr0 "[" term1_extended_list_opt "]" term1_extended_list      (* setoid_ring plugin *)
+| "field_lookup" ltac_expr "[" term1_extended_list_opt "]" term1_extended_list      (* setoid_ring plugin *)
 ]
 
-constr_with_bindings_opt: [
-| constr_with_bindings
-| empty
-]
-
-int_or_var_opt: [
-| int_or_var
-| empty
+int_or_var: [
+| int
+| ident
 ]
 
-uconstr_list_opt: [
-| uconstr_list_opt uconstr
+constr_with_bindings_opt: [
+| constr_with_bindings
 | empty
 ]
 
-constr_with_bindings_arg_list_comma: [
-| constr_with_bindings_arg_list_comma "," constr_with_bindings_arg
-| constr_with_bindings_arg
-]
-
-fixdecl_list: [
-| fixdecl_list fixdecl
-| fixdecl
-]
-
-cofixdecl_list: [
-| cofixdecl_list cofixdecl
-| cofixdecl
-]
-
-pattern_occ_list_opt: [
-| pattern_occ_list_opt "," pattern_occ as_name
+hloc: [
 | empty
+| "in" "|-" "*"
+| "in" ident
+| "in" "(" "Type" "of" ident ")"
+| "in" "(" "Value" "of" ident ")"
+| "in" "(" "type" "of" ident ")"
+| "in" "(" "value" "of" ident ")"
 ]
 
-oriented_rewriter_list_comma: [
-| oriented_rewriter_list_comma "," oriented_rewriter
-| oriented_rewriter
-]
-
-simple_alt: [
-| "simple" "inversion"
-| "inversion"
-| "inversion_clear"
+rename: [
+| ident "into" ident
 ]
 
-with_opt2: [
-| "with" term
+by_arg_tac: [
+| "by" ltac_expr3
 | empty
 ]
 
-tactic_opt: [
-| tactic
-| empty
+in_clause: [
+| in_clause
+| "*" occs
+| "*" "|-" concl_occ
+| hypident_occ_list_comma_opt "|-" concl_occ
+| hypident_occ_list_comma_opt
 ]
 
-reference_opt: [
-| reference
+occs: [
+| "at" occs_nums
 | empty
 ]
 
-bindings_list_comma: [
-| bindings_list_comma "," bindings
-| bindings
-]
-
-rename_list_comma: [
-| rename_list_comma "," rename
-| rename
-]
-
-orient_string: [
-| orient preident
-]
-
-comparison: [
-| "="
-| "<"
-| "<="
-| ">"
-| ">="
-]
-
-test: [
-| int_or_var comparison int_or_var
-]
-
-hintbases: [
-| "with" "*"
-| "with" preident_list
+hypident_occ_list_comma_opt: [
+| hypident_occ_list_comma
 | empty
 ]
 
-preident_list: [
-| preident_list preident
-| preident
-]
-
-auto_using: [
-| "using" uconstr_list_comma
+as_ipat: [
+| "as" simple_intropattern
 | empty
 ]
 
-uconstr_list_comma: [
-| uconstr_list_comma "," uconstr
-| uconstr
-]
-
-hints_path_atom: [
-| global_list
-| "_"
-]
-
-hints_path: [
-| "(" hints_path ")"
-| hints_path "*"
-| "emp"
-| "eps"
-| hints_path "|" hints_path
-| hints_path_atom
-| hints_path hints_path
+or_and_intropattern_loc: [
+| or_and_intropattern
+| ident
 ]
 
-opthints: [
-| ":" preident_list
+as_or_and_ipat: [
+| "as" or_and_intropattern_loc
 | empty
 ]
 
-debug: [
-| "debug"
+eqn_ipat: [
+| "eqn" ":" naming_intropattern
+| "_eqn" ":" naming_intropattern
+| "_eqn"
 | empty
 ]
 
-eauto_search_strategy: [
-| "(bfs)"
-| "(dfs)"
+as_name: [
+| "as" ident
 | empty
 ]
 
-glob_constr_with_bindings: [
-| constr_with_bindings
-]
-
-rewstrategy: [
-| glob
-| "<-" term
-| "subterms" rewstrategy
-| "subterm" rewstrategy
-| "innermost" rewstrategy
-| "outermost" rewstrategy
-| "bottomup" rewstrategy
-| "topdown" rewstrategy
-| "id"
-| "fail"
-| "refl"
-| "progress" rewstrategy
-| "try" rewstrategy
-| "any" rewstrategy
-| "repeat" rewstrategy
-| rewstrategy ";" rewstrategy
-| "(" rewstrategy ")"
-| "choice" rewstrategy rewstrategy
-| "old_hints" preident
-| "hints" preident
-| "terms" term_list_opt
-| "eval" red_expr
-| "fold" term
-]
-
-term_list_opt: [
-| term_list_opt term
+by_tactic: [
+| "by" ltac_expr3
 | empty
 ]
 
-int_or_var: [
-| integer
-| ident
-]
-
-nat_or_var: [
-| natural
-| ident
-]
-
-id_or_meta: [
-| ident
-]
-
-open_constr: [
-| term
-]
-
-uconstr: [
-| term
-]
-
-destruction_arg: [
-| natural
-| constr_with_bindings
+rewriter: [
+| "!" constr_with_bindings_arg
+| qmark_alt constr_with_bindings_arg
+| num "!" constr_with_bindings_arg
+| num qmark_alt constr_with_bindings_arg
+| num constr_with_bindings_arg
 | constr_with_bindings_arg
 ]
 
-constr_with_bindings_arg: [
-| ">" constr_with_bindings
-| constr_with_bindings
+qmark_alt: [
+| "?"
+| "?"
 ]
 
-quantified_hypothesis: [
-| ident
-| natural
+oriented_rewriter: [
+| orient rewriter
 ]
 
-conversion: [
-| term
-| term "with" term
-| term "at" occs_nums "with" term
+induction_clause: [
+| destruction_arg as_or_and_ipat eqn_ipat opt_clause
 ]
 
-occs_nums: [
-| nat_or_var_list
-| "-" nat_or_var int_or_var_list_opt
+induction_clause_list: [
+| induction_clause_list_comma eliminator_opt opt_clause
 ]
 
-nat_or_var_list: [
-| nat_or_var_list nat_or_var
-| nat_or_var
+induction_clause_list_comma: [
+| induction_clause_list_comma "," induction_clause
+| induction_clause
 ]
 
-int_or_var_list_opt: [
-| int_or_var_list_opt int_or_var
+eliminator_opt: [
+| "using" constr_with_bindings
 | empty
 ]
 
-occs: [
-| "at" occs_nums
+auto_using: [
+| "using" term1_extended_list_comma
 | empty
 ]
 
-pattern_occ: [
-| term occs
-]
-
-ref_or_pattern_occ: [
-| smart_global occs
-| term occs
-]
-
-unfold_occ: [
-| smart_global occs
+term1_extended_list_comma: [
+| term1_extended_list_comma "," term1_extended
+| term1_extended
 ]
 
 intropattern_list_opt: [
@@ -2764,11 +2492,11 @@ intropattern: [
 ]
 
 simple_intropattern: [
-| simple_intropattern_closed operconstr0_list_opt
+| simple_intropattern_closed term0_list_opt
 ]
 
-operconstr0_list_opt: [
-| operconstr0_list_opt "%" operconstr0
+term0_list_opt: [
+| term0_list_opt "%" term0
 | empty
 ]
 
@@ -2780,13 +2508,13 @@ simple_intropattern_closed: [
 ]
 
 simple_binding: [
-| "(" ident ":=" lconstr ")"
-| "(" natural ":=" lconstr ")"
+| "(" ident ":=" term ")"
+| "(" num ":=" term ")"
 ]
 
 bindings: [
 | simple_binding_list
-| term_list
+| term1_extended_list
 ]
 
 simple_binding_list: [
@@ -2794,88 +2522,88 @@ simple_binding_list: [
 | simple_binding
 ]
 
-term_list: [
-| term_list term
-| term
+constr_with_bindings_arg_list_comma: [
+| constr_with_bindings_arg_list_comma "," constr_with_bindings_arg
+| constr_with_bindings_arg
 ]
 
-constr_with_bindings: [
-| term with_bindings
+fixdecl_list: [
+| fixdecl_list fixdecl
+| fixdecl
 ]
 
-with_bindings: [
-| "with" bindings
+cofixdecl_list: [
+| cofixdecl_list cofixdecl
+| cofixdecl
+]
+
+pattern_occ_list_opt: [
+| pattern_occ_list_opt "," pattern_occ as_name
 | empty
 ]
 
-red_flags: [
-| "beta"
-| "iota"
-| "match"
-| "fix"
-| "cofix"
-| "zeta"
-| "delta" delta_flag
+pattern_occ: [
+| term1_extended occs
 ]
 
-delta_flag: [
-| "-" "[" smart_global_list "]"
-| "[" smart_global_list "]"
+oriented_rewriter_list_comma: [
+| oriented_rewriter_list_comma "," oriented_rewriter
+| oriented_rewriter
+]
+
+simple_alt: [
+| "simple" "inversion"
+| "inversion"
+| "inversion_clear"
+]
+
+with_opt2: [
+| "with" term1_extended
 | empty
 ]
 
-smart_global_list: [
-| smart_global_list smart_global
-| smart_global
+bindings_list_comma: [
+| bindings_list_comma "," bindings
+| bindings
 ]
 
-strategy_flag: [
-| red_flags_list
-| delta_flag
+rename_list_comma: [
+| rename_list_comma "," rename
+| rename
 ]
 
-red_flags_list: [
-| red_flags_list red_flags
-| red_flags
+comparison: [
+| "="
+| "<"
+| "<="
+| ">"
+| ">="
 ]
 
-red_expr: [
-| "red"
-| "hnf"
-| "simpl" delta_flag ref_or_pattern_occ_opt
-| "cbv" strategy_flag
-| "cbn" strategy_flag
-| "lazy" strategy_flag
-| "compute" delta_flag
-| "vm_compute" ref_or_pattern_occ_opt
-| "native_compute" ref_or_pattern_occ_opt
-| "unfold" unfold_occ_list_comma
-| "fold" term_list
-| "pattern" pattern_occ_list_comma
-| IDENT
+hintbases: [
+| "with" "*"
+| "with" ident_list
+| empty
 ]
 
-ref_or_pattern_occ_opt: [
-| ref_or_pattern_occ
+qualid_opt: [
+| qualid
 | empty
 ]
 
-unfold_occ_list_comma: [
-| unfold_occ_list_comma "," unfold_occ
-| unfold_occ
+bindings_with_parameters: [
+| "(" ident simple_binder_list_opt ":=" term ")"
 ]
 
-pattern_occ_list_comma: [
-| pattern_occ_list_comma "," pattern_occ
-| pattern_occ
+simple_binder_list_opt: [
+| simple_binder_list_opt simple_binder
+| empty
 ]
 
 hypident: [
-| id_or_meta
-| "(" "type" "of" id_or_meta ")"
-| "(" "value" "of" id_or_meta ")"
-| "(" "type" "of" ident ")"      (* ssr plugin *)
-| "(" "value" "of" ident ")"      (* ssr plugin *)
+| ident
+| "(" "type" "of" ident ")"
+| "(" "value" "of" ident ")"
 ]
 
 hypident_occ: [
@@ -2899,118 +2627,151 @@ opt_clause: [
 | empty
 ]
 
+occs_nums: [
+| num_or_var_list
+| "-" num_or_var int_or_var_list_opt
+]
+
+num_or_var: [
+| num
+| ident
+]
+
+int_or_var_list_opt: [
+| int_or_var_list_opt int_or_var
+| empty
+]
+
+num_or_var_list: [
+| num_or_var_list num_or_var
+| num_or_var
+]
+
 concl_occ: [
 | "*" occs
 | empty
 ]
 
 in_hyp_list: [
-| "in" id_or_meta_list
+| "in" ident_list
 | empty
 ]
 
-id_or_meta_list: [
-| id_or_meta_list id_or_meta
-| id_or_meta
-]
-
 in_hyp_as: [
-| "in" id_or_meta as_ipat
+| "in" ident as_ipat
 | empty
 ]
 
 simple_binder: [
 | name
-| "(" name_list ":" lconstr ")"
+| "(" names ":" term ")"
 ]
 
 fixdecl: [
-| "(" ident simple_binder_list_opt fixannot ":" lconstr ")"
+| "(" ident simple_binder_list_opt struct_annot ":" term ")"
 ]
 
-cofixdecl: [
-| "(" ident simple_binder_list_opt ":" lconstr ")"
-]
-
-bindings_with_parameters: [
-| "(" ident simple_binder_list_opt ":=" lconstr ")"
+struct_annot: [
+| "{" "struct" name "}"
+| empty
 ]
 
-simple_binder_list_opt: [
-| simple_binder_list_opt simple_binder
-| empty
+cofixdecl: [
+| "(" ident simple_binder_list_opt ":" term ")"
 ]
 
-eliminator: [
-| "using" constr_with_bindings
+constr_with_bindings: [
+| term1_extended with_bindings
 ]
 
-as_ipat: [
-| "as" simple_intropattern
+with_bindings: [
+| "with" bindings
 | empty
 ]
 
-or_and_intropattern_loc: [
-| or_and_intropattern
-| ident
+destruction_arg: [
+| num
+| constr_with_bindings
+| constr_with_bindings_arg
 ]
 
-as_or_and_ipat: [
-| "as" or_and_intropattern_loc
-| empty
+constr_with_bindings_arg: [
+| ">" constr_with_bindings
+| constr_with_bindings
 ]
 
-eqn_ipat: [
-| "eqn" ":" naming_intropattern
-| "_eqn" ":" naming_intropattern
-| "_eqn"
-| empty
+quantified_hypothesis: [
+| ident
+| num
 ]
 
-as_name: [
-| "as" ident
-| empty
+conversion: [
+| term1_extended
+| term1_extended "with" term1_extended
+| term1_extended "at" occs_nums "with" term1_extended
 ]
 
-by_tactic: [
-| "by" ltac_expr3
+firstorder_using: [
+| "using" qualid
+| "using" qualid "," qualid_list_comma
+| "using" qualid qualid qualid_list_opt
 | empty
 ]
 
-rewriter: [
-| "!" constr_with_bindings_arg
-| qmark_alt constr_with_bindings_arg
-| natural "!" constr_with_bindings_arg
-| natural qmark_alt constr_with_bindings_arg
-| natural constr_with_bindings_arg
-| constr_with_bindings_arg
+qualid_list_comma: [
+| qualid_list_comma "," qualid
+| qualid
 ]
 
-qmark_alt: [
-| "?"
-| "?"
+fun_ind_using: [
+| "using" constr_with_bindings      (* funind plugin *)
+| empty      (* funind plugin *)
 ]
 
-oriented_rewriter: [
-| orient rewriter
+with_names: [
+| "as" simple_intropattern      (* funind plugin *)
+| empty      (* funind plugin *)
 ]
 
-induction_clause: [
-| destruction_arg as_or_and_ipat eqn_ipat opt_clause
+occurrences: [
+| int_list
+| ident
 ]
 
-induction_clause_list: [
-| induction_clause_list_comma eliminator_opt opt_clause
+int_list: [
+| int_list int
+| int
 ]
 
-induction_clause_list_comma: [
-| induction_clause_list_comma "," induction_clause
-| induction_clause
+rewstrategy: [
+| term1_extended
+| "<-" term1_extended
+| "subterms" rewstrategy
+| "subterm" rewstrategy
+| "innermost" rewstrategy
+| "outermost" rewstrategy
+| "bottomup" rewstrategy
+| "topdown" rewstrategy
+| "id"
+| "fail"
+| "refl"
+| "progress" rewstrategy
+| "try" rewstrategy
+| "any" rewstrategy
+| "repeat" rewstrategy
+| rewstrategy ";" rewstrategy
+| "(" rewstrategy ")"
+| "choice" rewstrategy rewstrategy
+| "old_hints" ident
+| "hints" ident
+| "terms" term1_extended_list_opt
+| "eval" red_expr
+| "fold" term1_extended
 ]
 
-eliminator_opt: [
-| eliminator
-| empty
+hypident_occ_list_comma: [
+| hypident_occ_list_comma "," hypident_occ
+| hypident_occ
 ]
 
 ltac_expr: [
@@ -3019,19 +2780,19 @@ ltac_expr: [
 ]
 
 binder_tactic: [
-| "fun" input_fun_list "=>" ltac_expr
+| "fun" fun_var_list "=>" ltac_expr
 | "let" rec_opt let_clause_list "in" ltac_expr
 | "info" ltac_expr
 ]
 
-input_fun_list: [
-| input_fun_list input_fun
-| input_fun
+fun_var_list: [
+| fun_var_list fun_var
+| fun_var
 ]
 
-input_fun: [
-| "_"
+fun_var: [
 | ident
+| "_"
 ]
 
 rec_opt: [
@@ -3047,27 +2808,20 @@ let_clause_list: [
 let_clause: [
 | ident ":=" ltac_expr
 | "_" ":=" ltac_expr
-| ident input_fun_list ":=" ltac_expr
+| ident fun_var_list ":=" ltac_expr
 ]
 
 ltac_expr4: [
 | ltac_expr3 ";" binder_tactic
 | ltac_expr3 ";" ltac_expr3
-| ltac_expr3 ";" "[" gt_opt tactic_then_gen "]"
+| ltac_expr3 ";" "[" multi_goal_tactics "]"
+| ltac_expr3 ";" "[" ">" multi_goal_tactics "]"
 | ltac_expr3
-| ltac_expr ";" "first" ssr_first_else      (* ssr plugin *)
-| ltac_expr ";" "first" ssrseqarg      (* ssr plugin *)
-| ltac_expr ";" "last" ssrseqarg      (* ssr plugin *)
-]
-
-gt_opt: [
-| ">"
-| empty
 ]
 
-tactic_then_gen: [
-| ltac_expr_opt "|" tactic_then_gen
-| ltac_expr_opt ".." or_opt ltac_expr_list2
+multi_goal_tactics: [
+| ltac_expr_opt "|" multi_goal_tactics
+| ltac_expr_opt ".." or_opt ltac_expr_opt_list_or
 | ltac_expr
 | empty
 ]
@@ -3077,13 +2831,8 @@ ltac_expr_opt: [
 | empty
 ]
 
-ltac_expr_list_or2_opt: [
-| ltac_expr_list_or2
-| empty
-]
-
-ltac_expr_list_or2: [
-| ltac_expr_list_or2 "|" ltac_expr_opt
+ltac_expr_opt_list_or: [
+| ltac_expr_opt_list_or "|" ltac_expr_opt
 | ltac_expr_opt
 ]
 
@@ -3099,51 +2848,10 @@ ltac_expr3: [
 | "infoH" ltac_expr3
 | "abstract" ltac_expr2
 | "abstract" ltac_expr2 "using" ident
-| selector ltac_expr3
-| "do" ssrmmod ssrdotac ssrclauses      (* ssr plugin *)
-| "do" ssrortacarg ssrclauses      (* ssr plugin *)
-| "do" int_or_var ssrmmod ssrdotac ssrclauses      (* ssr plugin *)
-| "abstract" ssrdgens      (* ssr plugin *)
+| only_selector ltac_expr3
 | ltac_expr2
 ]
 
-tactic_mode: [
-| toplevel_selector_opt query_command
-| toplevel_selector_opt "{"
-| toplevel_selector_opt ltac_info_opt tactic ltac_use_default
-| "par" ":" ltac_info_opt tactic ltac_use_default
-]
-
-toplevel_selector_opt: [
-| toplevel_selector
-| empty
-]
-
-toplevel_selector: [
-| selector_body ":"
-| "!" ":"
-| "all" ":"
-]
-
-selector: [
-| "only" selector_body ":"
-]
-
-selector_body: [
-| range_selector_list_comma
-| "[" ident "]"
-]
-
-range_selector_list_comma: [
-| range_selector_list_comma "," range_selector
-| range_selector
-]
-
-range_selector: [
-| natural "-" natural
-| natural
-]
-
 ltac_expr2: [
 | ltac_expr1 "+" binder_tactic
 | ltac_expr1 "+" ltac_expr2
@@ -3154,30 +2862,18 @@ ltac_expr2: [
 ]
 
 ltac_expr1: [
-| match_key reverse_opt "goal" "with" match_context_list "end"
-| match_key ltac_expr "with" match_list "end"
+| ltac_match_term
+| ltac_match_goal
 | "first" "[" ltac_expr_list_or_opt "]"
 | "solve" "[" ltac_expr_list_or_opt "]"
 | "idtac" message_token_list_opt
 | failkw int_or_var_opt message_token_list_opt
 | simple_tactic
 | tactic_arg
-| reference tactic_arg_compat_list_opt
-| ltac_expr ssrintros_ne      (* ssr plugin *)
+| qualid tactic_arg_compat_list_opt
 | ltac_expr0
 ]
 
-match_key: [
-| "match"
-| "lazymatch"
-| "multimatch"
-]
-
-reverse_opt: [
-| "reverse"
-| empty
-]
-
 ltac_expr_list_or_opt: [
 | ltac_expr_list_or
 | empty
@@ -3188,95 +2884,27 @@ ltac_expr_list_or: [
 | ltac_expr
 ]
 
-match_context_list: [
-| or_opt match_context_rule_list_or
-]
-
-match_context_rule_list_or: [
-| match_context_rule_list_or "|" match_context_rule
-| match_context_rule
-]
-
-or_opt: [
-| "|"
-| empty
-]
-
-eqn_list_or_opt: [
-| eqn_list_or
-| empty
-]
-
-eqn_list_or: [
-| eqn_list_or "|" eqn
-| eqn
-]
-
-match_context_rule: [
-| match_hyps_list_comma_opt "|-" match_pattern "=>" ltac_expr
-| "[" match_hyps_list_comma_opt "|-" match_pattern "]" "=>" ltac_expr
-| "_" "=>" ltac_expr
-]
-
-match_hyps_list_comma_opt: [
-| match_hyps_list_comma
+message_token_list_opt: [
+| message_token_list_opt message_token
 | empty
 ]
 
-match_hyps_list_comma: [
-| match_hyps_list_comma "," match_hyps
-| match_hyps
-]
-
-match_hyps: [
-| name ":" match_pattern
-| name ":=" match_pattern_opt match_pattern
-]
-
-match_pattern: [
-| "context" ident_opt "[" lconstr_pattern "]"
-| lconstr_pattern
-]
-
-ident_opt: [
+message_token: [
 | ident
-| empty
-]
-
-lconstr_pattern: [
-| lconstr
+| string
+| int
 ]
 
-match_pattern_opt: [
-| "[" match_pattern "]" ":"
+int_or_var_opt: [
+| int_or_var
 | empty
 ]
 
-match_list: [
-| or_opt match_rule_list_or
-]
-
-match_rule_list_or: [
-| match_rule_list_or "|" match_rule
-| match_rule
-]
-
-match_rule: [
-| match_pattern "=>" ltac_expr
-| "_" "=>" ltac_expr
-]
-
-message_token_list_opt: [
-| message_token_list_opt message_token
+term1_extended_list_opt: [
+| term1_extended_list_opt term1_extended
 | empty
 ]
 
-message_token: [
-| ident
-| STRING
-| integer
-]
-
 failkw: [
 | "fail"
 | "gfail"
@@ -3284,10 +2912,10 @@ failkw: [
 
 tactic_arg: [
 | "eval" red_expr "in" term
-| "context" ident "[" lconstr "]"
+| "context" ident "[" term "]"
 | "type" "of" term
 | "fresh" fresh_id_list_opt
-| "type_term" uconstr
+| "type_term" term1_extended
 | "numgoals"
 ]
 
@@ -3297,7 +2925,7 @@ fresh_id_list_opt: [
 ]
 
 fresh_id: [
-| STRING
+| string
 | qualid
 ]
 
@@ -3314,857 +2942,112 @@ tactic_arg_compat: [
 
 ltac_expr0: [
 | "(" ltac_expr ")"
-| "[" ">" tactic_then_gen "]"
+| "[>" multi_goal_tactics "]"
 | tactic_atom
-| ssrparentacarg      (* ssr plugin *)
 ]
 
 tactic_atom: [
-| integer
-| reference
+| int
+| qualid
 | "()"
 ]
 
-constr_may_eval: [
-| "eval" red_expr "in" term
-| "context" ident "[" lconstr "]"
-| "type" "of" term
-| term
-]
-
-ltac_def_kind: [
-| ":="
-| "::="
-]
-
-tacdef_body: [
-| global input_fun_list ltac_def_kind ltac_expr
-| global ltac_def_kind ltac_expr
+toplevel_selector: [
+| selector ":"
+| "all" ":"
+| "!" ":"
 ]
 
-tactic: [
-| ltac_expr
+only_selector: [
+| "only" selector ":"
 ]
 
-ltac_info_opt: [
-| ltac_info
-| empty
+selector: [
+| range_selector_list_comma
+| "[" ident "]"
 ]
 
-ltac_info: [
-| "Info" natural
+range_selector_list_comma: [
+| range_selector_list_comma "," range_selector
+| range_selector
 ]
 
-ltac_use_default: [
-| "."
-| "..."
+range_selector: [
+| num "-" num
+| num
 ]
 
-ltac_tactic_level: [
-| "(" "at" "level" natural ")"
+ltac_match_term: [
+| match_key ltac_expr "with" or_opt match_rule_list_or "end"
 ]
 
-ltac_production_sep: [
-| "," string
+match_key: [
+| "match"
+| "multimatch"
+| "lazymatch"
 ]
 
-ltac_production_item: [
-| string
-| ident "(" ident ltac_production_sep_opt ")"
-| ident
+match_rule_list_or: [
+| match_rule_list_or "|" match_rule
+| match_rule
 ]
 
-ltac_production_sep_opt: [
-| ltac_production_sep
-| empty
+match_rule: [
+| match_pattern_alt "=>" ltac_expr
 ]
 
-ltac_tacdef_body: [
-| tacdef_body
+match_pattern_alt: [
+| match_pattern
+| "_"
 ]
 
-firstorder_using: [
-| "using" reference
-| "using" reference "," reference_list_comma
-| "using" reference reference reference_list_opt
-| empty
+match_pattern: [
+| "context" ident_opt "[" term "]"
+| term
 ]
 
-reference_list_comma: [
-| reference_list_comma "," reference
-| reference
+ltac_match_goal: [
+| match_key reverse_opt "goal" "with" or_opt match_context_rule_list_or "end"
 ]
 
-numnotoption: [
+reverse_opt: [
+| "reverse"
 | empty
-| "(" "warning" "after" bigint ")"
-| "(" "abstract" "after" bigint ")"
-]
-
-mlname: [
-| preident      (* extraction plugin *)
-| string      (* extraction plugin *)
-]
-
-int_or_id: [
-| preident      (* extraction plugin *)
-| integer      (* extraction plugin *)
-]
-
-language: [
-| "Ocaml"      (* extraction plugin *)
-| "OCaml"      (* extraction plugin *)
-| "Haskell"      (* extraction plugin *)
-| "Scheme"      (* extraction plugin *)
-| "JSON"      (* extraction plugin *)
-]
-
-fun_ind_using: [
-| "using" constr_with_bindings      (* funind plugin *)
-| empty      (* funind plugin *)
-]
-
-with_names: [
-| "as" simple_intropattern      (* funind plugin *)
-| empty      (* funind plugin *)
-]
-
-constr_comma_sequence': [
-| term "," constr_comma_sequence'      (* funind plugin *)
-| term      (* funind plugin *)
-]
-
-auto_using': [
-| "using" constr_comma_sequence'      (* funind plugin *)
-| empty      (* funind plugin *)
-]
-
-function_rec_definition_loc: [
-| rec_definition      (* funind plugin *)
-]
-
-fun_scheme_arg: [
-| ident ":=" "Induction" "for" reference "Sort" sort_family      (* funind plugin *)
-]
-
-ring_mod: [
-| "decidable" term      (* setoid_ring plugin *)
-| "abstract"      (* setoid_ring plugin *)
-| "morphism" term      (* setoid_ring plugin *)
-| "constants" "[" tactic "]"      (* setoid_ring plugin *)
-| "closed" "[" global_list "]"      (* setoid_ring plugin *)
-| "preprocess" "[" tactic "]"      (* setoid_ring plugin *)
-| "postprocess" "[" tactic "]"      (* setoid_ring plugin *)
-| "setoid" term term      (* setoid_ring plugin *)
-| "sign" term      (* setoid_ring plugin *)
-| "power" term "[" global_list "]"      (* setoid_ring plugin *)
-| "power_tac" term "[" tactic "]"      (* setoid_ring plugin *)
-| "div" term      (* setoid_ring plugin *)
-]
-
-ring_mods: [
-| "(" ring_mod_list_comma ")"      (* setoid_ring plugin *)
-]
-
-ring_mod_list_comma: [
-| ring_mod_list_comma "," ring_mod
-| ring_mod
-]
-
-field_mod: [
-| ring_mod      (* setoid_ring plugin *)
-| "completeness" term      (* setoid_ring plugin *)
-]
-
-field_mods: [
-| "(" field_mod_list_comma ")"      (* setoid_ring plugin *)
-]
-
-field_mod_list_comma: [
-| field_mod_list_comma "," field_mod
-| field_mod
-]
-
-ssrtacarg: [
-| ltac_expr      (* ssr plugin *)
-]
-
-ssrtac3arg: [
-| ltac_expr3      (* ssr plugin *)
-]
-
-ssrtclarg: [
-| ssrtacarg      (* ssr plugin *)
-]
-
-ssrhyp: [
-| ident      (* ssr plugin *)
-]
-
-ssrhoi_hyp: [
-| ident      (* ssr plugin *)
-]
-
-ssrhoi_id: [
-| ident      (* ssr plugin *)
 ]
 
-ssrsimpl_ne: [
-| "//="      (* ssr plugin *)
-| "/="      (* ssr plugin *)
-| "/" natural "/" natural "="      (* ssr plugin *)
-| "/" natural "/"      (* ssr plugin *)
-| "/" natural "="      (* ssr plugin *)
-| "/" natural "/="      (* ssr plugin *)
-| "/" natural "/" "="      (* ssr plugin *)
-| "//" natural "="      (* ssr plugin *)
-| "//"      (* ssr plugin *)
-]
-
-ssrclear_ne: [
-| "{" ssrhyp_list "}"      (* ssr plugin *)
-]
-
-ssrclear: [
-| ssrclear_ne      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssrindex: [
-| int_or_var      (* ssr plugin *)
+match_context_rule_list_or: [
+| match_context_rule_list_or "|" match_context_rule
+| match_context_rule
 ]
 
-ssrocc: [
-| natural natural_list_opt      (* ssr plugin *)
-| "-" natural_list_opt      (* ssr plugin *)
-| "+" natural_list_opt      (* ssr plugin *)
+match_context_rule: [
+| match_hyp_list_comma_opt "|-" match_pattern "=>" ltac_expr
+| "[" match_hyp_list_comma_opt "|-" match_pattern "]" "=>" ltac_expr
+| "_" "=>" ltac_expr
 ]
 
-natural_list_opt: [
-| natural_list_opt natural
+match_hyp_list_comma_opt: [
+| match_hyp_list_comma
 | empty
 ]
 
-ssrmmod: [
-| "!"      (* ssr plugin *)
-| "?"      (* ssr plugin *)
-| "?"      (* ssr plugin *)
-]
-
-ssrmult_ne: [
-| natural ssrmmod      (* ssr plugin *)
-| ssrmmod      (* ssr plugin *)
-]
-
-ssrmult: [
-| ssrmult_ne      (* ssr plugin *)
-| empty      (* ssr plugin *)
+match_hyp_list_comma: [
+| match_hyp_list_comma "," match_hyp
+| match_hyp
 ]
 
-ssrdocc: [
-| "{" ssrocc "}"      (* ssr plugin *)
-| "{" ssrhyp_list_opt "}"      (* ssr plugin *)
+match_hyp: [
+| name ":" match_pattern
+| name ":=" match_pattern_opt match_pattern
 ]
 
-ssrhyp_list_opt: [
-| ssrhyp_list_opt ssrhyp
+match_pattern_opt: [
+| "[" match_pattern "]" ":"
 | empty
 ]
 
-ssrterm: [
-| "YouShouldNotTypeThis" term      (* ssr plugin *)
-| term      (* ssr plugin *)
-]
-
-ast_closure_term: [
-| term      (* ssr plugin *)
-]
-
-ast_closure_lterm: [
-| lconstr      (* ssr plugin *)
-]
-
-ssrbwdview: [
-| "YouShouldNotTypeThis"      (* ssr plugin *)
-| "/" term      (* ssr plugin *)
-| "/" term ssrbwdview      (* ssr plugin *)
-]
-
-ssrfwdview: [
-| "YouShouldNotTypeThis"      (* ssr plugin *)
-| "/" ast_closure_term      (* ssr plugin *)
-| "/" ast_closure_term ssrfwdview      (* ssr plugin *)
-]
-
-ident_no_do: [
-| "YouShouldNotTypeThis" ident      (* ssr plugin *)
-| IDENT      (* ssr plugin *)
-]
-
-ssripat: [
-| "_"      (* ssr plugin *)
-| "*"      (* ssr plugin *)
-| ">"      (* ssr plugin *)
-| ident_no_do      (* ssr plugin *)
-| "?"      (* ssr plugin *)
-| "+"      (* ssr plugin *)
-| "++"      (* ssr plugin *)
-| ssrsimpl_ne      (* ssr plugin *)
-| ssrdocc "->"      (* ssr plugin *)
-| ssrdocc "<-"      (* ssr plugin *)
-| ssrdocc      (* ssr plugin *)
-| "->"      (* ssr plugin *)
-| "<-"      (* ssr plugin *)
-| "-"      (* ssr plugin *)
-| "-/" "="      (* ssr plugin *)
-| "-/="      (* ssr plugin *)
-| "-/" "/"      (* ssr plugin *)
-| "-//"      (* ssr plugin *)
-| "-/" integer "/"      (* ssr plugin *)
-| "-/" "/="      (* ssr plugin *)
-| "-//" "="      (* ssr plugin *)
-| "-//="      (* ssr plugin *)
-| "-/" integer "/="      (* ssr plugin *)
-| "-/" integer "/" integer "="      (* ssr plugin *)
-| ssrfwdview      (* ssr plugin *)
-| "[" ":" ident_list_opt "]"      (* ssr plugin *)
-| "[:" ident_list_opt "]"      (* ssr plugin *)
-| ssrcpat      (* ssr plugin *)
-]
-
 ident_list_opt: [
 | ident_list_opt ident
 | empty
 ]
 
-ssripats: [
-| ssripat ssripats      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssriorpat: [
-| ssripats "|" ssriorpat      (* ssr plugin *)
-| ssripats "|-" ">" ssriorpat      (* ssr plugin *)
-| ssripats "|-" ssriorpat      (* ssr plugin *)
-| ssripats "|->" ssriorpat      (* ssr plugin *)
-| ssripats "||" ssriorpat      (* ssr plugin *)
-| ssripats "|||" ssriorpat      (* ssr plugin *)
-| ssripats "||||" ssriorpat      (* ssr plugin *)
-| ssripats      (* ssr plugin *)
-]
-
-ssrcpat: [
-| "YouShouldNotTypeThis" ssriorpat      (* ssr plugin *)
-| "[" hat "]"      (* ssr plugin *)
-| "[" ssriorpat "]"      (* ssr plugin *)
-| "[=" ssriorpat "]"      (* ssr plugin *)
-]
-
-hat: [
-| "^" ident      (* ssr plugin *)
-| "^" "~" ident      (* ssr plugin *)
-| "^" "~" natural      (* ssr plugin *)
-| "^~" ident      (* ssr plugin *)
-| "^~" natural      (* ssr plugin *)
-]
-
-ssripats_ne: [
-| ssripat ssripats      (* ssr plugin *)
-]
-
-ssrhpats: [
-| ssripats      (* ssr plugin *)
-]
-
-ssrhpats_wtransp: [
-| ssripats      (* ssr plugin *)
-| ssripats "@" ssripats      (* ssr plugin *)
-]
-
-ssrhpats_nobs: [
-| ssripats      (* ssr plugin *)
-]
-
-ssrrpat: [
-| "->"      (* ssr plugin *)
-| "<-"      (* ssr plugin *)
-]
-
-ssrintros_ne: [
-| "=>" ssripats_ne      (* ssr plugin *)
-]
-
-ssrintros: [
-| ssrintros_ne      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssrintrosarg: [
-| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne      (* ssr plugin *)
-]
-
-ssrfwdid: [
-| ident      (* ssr plugin *)
-]
-
-ssrortacs: [
-| ssrtacarg "|" ssrortacs      (* ssr plugin *)
-| ssrtacarg "|"      (* ssr plugin *)
-| ssrtacarg      (* ssr plugin *)
-| "|" ssrortacs      (* ssr plugin *)
-| "|"      (* ssr plugin *)
-]
-
-ssrhintarg: [
-| "[" "]"      (* ssr plugin *)
-| "[" ssrortacs "]"      (* ssr plugin *)
-| ssrtacarg      (* ssr plugin *)
-]
-
-ssrhint3arg: [
-| "[" "]"      (* ssr plugin *)
-| "[" ssrortacs "]"      (* ssr plugin *)
-| ssrtac3arg      (* ssr plugin *)
-]
-
-ssrortacarg: [
-| "[" ssrortacs "]"      (* ssr plugin *)
-]
-
-ssrhint: [
-| empty      (* ssr plugin *)
-| "by" ssrhintarg      (* ssr plugin *)
-]
-
-ssrwgen: [
-| ssrclear_ne      (* ssr plugin *)
-| ssrhoi_hyp      (* ssr plugin *)
-| "@" ssrhoi_hyp      (* ssr plugin *)
-| "(" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
-| "(" ssrhoi_id ")"      (* ssr plugin *)
-| "(@" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
-| "(" "@" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
-]
-
-ssrclausehyps: [
-| ssrwgen "," ssrclausehyps      (* ssr plugin *)
-| ssrwgen ssrclausehyps      (* ssr plugin *)
-| ssrwgen      (* ssr plugin *)
-]
-
-ssrclauses: [
-| "in" ssrclausehyps "|-" "*"      (* ssr plugin *)
-| "in" ssrclausehyps "|-"      (* ssr plugin *)
-| "in" ssrclausehyps "*"      (* ssr plugin *)
-| "in" ssrclausehyps      (* ssr plugin *)
-| "in" "|-" "*"      (* ssr plugin *)
-| "in" "*"      (* ssr plugin *)
-| "in" "*" "|-"      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssrfwd: [
-| ":=" ast_closure_lterm      (* ssr plugin *)
-| ":" ast_closure_lterm ":=" ast_closure_lterm      (* ssr plugin *)
-]
-
-ssrbvar: [
-| ident      (* ssr plugin *)
-| "_"      (* ssr plugin *)
-]
-
-ssrbinder: [
-| ssrbvar      (* ssr plugin *)
-| "(" ssrbvar ")"      (* ssr plugin *)
-| "(" ssrbvar ":" lconstr ")"      (* ssr plugin *)
-| "(" ssrbvar ssrbvar_list ":" lconstr ")"      (* ssr plugin *)
-| "(" ssrbvar ":" lconstr ":=" lconstr ")"      (* ssr plugin *)
-| "(" ssrbvar ":=" lconstr ")"      (* ssr plugin *)
-| of_alt operconstr99      (* ssr plugin *)
-]
-
-ssrbvar_list: [
-| ssrbvar_list ssrbvar
-| ssrbvar
-]
-
-ssrstruct: [
-| "{" "struct" ident "}"      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssrposefwd: [
-| ssrbinder_list_opt ssrfwd      (* ssr plugin *)
-]
-
-ssrfixfwd: [
-| "fix" ssrbvar ssrbinder_list_opt ssrstruct ssrfwd      (* ssr plugin *)
-]
-
-ssrcofixfwd: [
-| "cofix" ssrbvar ssrbinder_list_opt ssrfwd      (* ssr plugin *)
-]
-
-ssrbinder_list_opt: [
-| ssrbinder_list_opt ssrbinder
-| empty
-]
-
-ssrsetfwd: [
-| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern      (* ssr plugin *)
-| ":" ast_closure_lterm ":=" lcpattern      (* ssr plugin *)
-| ":=" "{" ssrocc "}" cpattern      (* ssr plugin *)
-| ":=" lcpattern      (* ssr plugin *)
-]
-
-ssrhavefwd: [
-| ":" ast_closure_lterm ssrhint      (* ssr plugin *)
-| ":" ast_closure_lterm ":=" ast_closure_lterm      (* ssr plugin *)
-| ":" ast_closure_lterm ":="      (* ssr plugin *)
-| ":=" ast_closure_lterm      (* ssr plugin *)
-]
-
-ssrhavefwdwbinders: [
-| ssrhpats_wtransp ssrbinder_list_opt ssrhavefwd      (* ssr plugin *)
-]
-
-ssrseqarg: [
-| ssrswap      (* ssr plugin *)
-| ssrseqidx ssrortacarg ssrorelse_opt      (* ssr plugin *)
-| ssrseqidx ssrswap      (* ssr plugin *)
-| ltac_expr3      (* ssr plugin *)
-]
-
-ssrorelse_opt: [
-| ssrorelse
-| empty
-]
-
-ssrseqidx: [
-| ident      (* ssr plugin *)
-| natural      (* ssr plugin *)
-]
-
-ssrswap: [
-| "first"      (* ssr plugin *)
-| "last"      (* ssr plugin *)
-]
-
-ssrorelse: [
-| "||" ltac_expr2      (* ssr plugin *)
-]
-
-ident: [
-| IDENT
-]
-
-ssrparentacarg: [
-| "(" ltac_expr ")"      (* ssr plugin *)
-]
-
-ssrdotac: [
-| ltac_expr3      (* ssr plugin *)
-| ssrortacarg      (* ssr plugin *)
-]
-
-ssr_first: [
-| ssr_first ssrintros_ne      (* ssr plugin *)
-| "[" ltac_expr_list_or_opt "]"      (* ssr plugin *)
-]
-
-ssr_first_else: [
-| ssr_first ssrorelse      (* ssr plugin *)
-| ssr_first      (* ssr plugin *)
-]
-
-ssrgen: [
-| ssrdocc cpattern      (* ssr plugin *)
-| cpattern      (* ssr plugin *)
-]
-
-ssrdgens_tl: [
-| "{" ssrhyp_list "}" cpattern ssrdgens_tl      (* ssr plugin *)
-| "{" ssrhyp_list "}"      (* ssr plugin *)
-| "{" ssrocc "}" cpattern ssrdgens_tl      (* ssr plugin *)
-| "/" ssrdgens_tl      (* ssr plugin *)
-| cpattern ssrdgens_tl      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssrdgens: [
-| ":" ssrgen ssrdgens_tl      (* ssr plugin *)
-]
-
-ssreqid: [
-| ssreqpat      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssreqpat: [
-| ident      (* ssr plugin *)
-| "_"      (* ssr plugin *)
-| "?"      (* ssr plugin *)
-| "+"      (* ssr plugin *)
-| ssrdocc "->"      (* ssr plugin *)
-| ssrdocc "<-"      (* ssr plugin *)
-| "->"      (* ssr plugin *)
-| "<-"      (* ssr plugin *)
-]
-
-ssrarg: [
-| ssrfwdview ssreqid ssrdgens ssrintros      (* ssr plugin *)
-| ssrfwdview ssrclear ssrintros      (* ssr plugin *)
-| ssreqid ssrdgens ssrintros      (* ssr plugin *)
-| ssrclear_ne ssrintros      (* ssr plugin *)
-| ssrintros_ne      (* ssr plugin *)
-]
-
-ssrmovearg: [
-| ssrarg      (* ssr plugin *)
-]
-
-ssrcasearg: [
-| ssrarg      (* ssr plugin *)
-]
-
-ssragen: [
-| "{" ssrhyp_list "}" ssrterm      (* ssr plugin *)
-| ssrterm      (* ssr plugin *)
-]
-
-ssrhyp_list: [
-| ssrhyp_list ssrhyp
-| ssrhyp
-]
-
-ssragens: [
-| "{" ssrhyp_list "}" ssrterm ssragens      (* ssr plugin *)
-| "{" ssrhyp_list "}"      (* ssr plugin *)
-| ssrterm ssragens      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssrapplyarg: [
-| ":" ssragen ssragens ssrintros      (* ssr plugin *)
-| ssrclear_ne ssrintros      (* ssr plugin *)
-| ssrintros_ne      (* ssr plugin *)
-| ssrbwdview ":" ssragen ssragens ssrintros      (* ssr plugin *)
-| ssrbwdview ssrclear ssrintros      (* ssr plugin *)
-]
-
-ssrexactarg: [
-| ":" ssragen ssragens      (* ssr plugin *)
-| ssrbwdview ssrclear      (* ssr plugin *)
-| ssrclear_ne      (* ssr plugin *)
-]
-
-ssrcongrarg: [
-| natural term ssrdgens      (* ssr plugin *)
-| natural term      (* ssr plugin *)
-| term ssrdgens      (* ssr plugin *)
-| term      (* ssr plugin *)
-]
-
-ssrrwocc: [
-| "{" ssrhyp_list_opt "}"      (* ssr plugin *)
-| "{" ssrocc "}"      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssrrule_ne: [
-| ssrterm_alt      (* ssr plugin *)
-| ssrsimpl_ne      (* ssr plugin *)
-]
-
-ssrterm_alt: [
-| "/" ssrterm
-| ssrterm
-| ssrsimpl_ne
-]
-
-ssrrule: [
-| ssrrule_ne      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssrpattern_squarep: [
-| "[" rpattern "]"      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssrpattern_ne_squarep: [
-| "[" rpattern "]"      (* ssr plugin *)
-]
-
-ssrrwarg: [
-| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
-| "-/" ssrterm      (* ssr plugin *)
-| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
-| "{" ssrhyp_list "}" ssrpattern_ne_squarep ssrrule_ne      (* ssr plugin *)
-| "{" ssrhyp_list "}" ssrrule      (* ssr plugin *)
-| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
-| "{" "}" ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
-| ssrpattern_ne_squarep ssrrule_ne      (* ssr plugin *)
-| ssrrule_ne      (* ssr plugin *)
-]
-
-ssrrwargs: [
-| ssrrwarg_list      (* ssr plugin *)
-]
-
-ssrrwarg_list: [
-| ssrrwarg_list ssrrwarg
-| ssrrwarg
-]
-
-ssrunlockarg: [
-| "{" ssrocc "}" ssrterm      (* ssr plugin *)
-| ssrterm      (* ssr plugin *)
-]
-
-ssrunlockargs: [
-| ssrunlockarg_list_opt      (* ssr plugin *)
-]
-
-ssrunlockarg_list_opt: [
-| ssrunlockarg_list_opt ssrunlockarg
-| empty
-]
-
-ssrsufffwd: [
-| ssrhpats ssrbinder_list_opt ":" ast_closure_lterm ssrhint      (* ssr plugin *)
-]
-
-ssrwlogfwd: [
-| ":" ssrwgen_list_opt "/" ast_closure_lterm      (* ssr plugin *)
-]
-
-ssrwgen_list_opt: [
-| ssrwgen_list_opt ssrwgen
-| empty
-]
-
-ssr_idcomma: [
-| empty      (* ssr plugin *)
-| IDENT_alt ","      (* ssr plugin *)
-]
-
-IDENT_alt: [
-| IDENT
-| "_"
-]
-
-ssr_rtype: [
-| "return" operconstr100      (* ssr plugin *)
-]
-
-ssr_mpat: [
-| pattern200      (* ssr plugin *)
-]
-
-ssr_dpat: [
-| ssr_mpat "in" pattern200 ssr_rtype      (* ssr plugin *)
-| ssr_mpat ssr_rtype      (* ssr plugin *)
-| ssr_mpat      (* ssr plugin *)
-]
-
-ssr_dthen: [
-| ssr_dpat "then" lconstr      (* ssr plugin *)
-]
-
-ssr_elsepat: [
-| "else"      (* ssr plugin *)
-]
-
-ssr_else: [
-| ssr_elsepat lconstr      (* ssr plugin *)
-]
-
-ssr_search_item: [
-| string      (* ssr plugin *)
-| string "%" preident      (* ssr plugin *)
-| constr_pattern      (* ssr plugin *)
-]
-
-ssr_search_arg: [
-| "-" ssr_search_item ssr_search_arg      (* ssr plugin *)
-| ssr_search_item ssr_search_arg      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssr_modlocs: [
-| empty      (* ssr plugin *)
-| "in" modloc_list      (* ssr plugin *)
-]
-
-modloc_list: [
-| modloc_list modloc
-| modloc
-]
-
-modloc: [
-| "-" global      (* ssr plugin *)
-| global      (* ssr plugin *)
-]
-
-ssrhintref: [
-| term      (* ssr plugin *)
-| term "|" natural      (* ssr plugin *)
-]
-
-ssrviewpos: [
-| "for" "move" "/"      (* ssr plugin *)
-| "for" "apply" "/"      (* ssr plugin *)
-| "for" "apply" "/" "/"      (* ssr plugin *)
-| "for" "apply" "//"      (* ssr plugin *)
-| empty      (* ssr plugin *)
-]
-
-ssrviewposspc: [
-| ssrviewpos      (* ssr plugin *)
-]
-
-rpattern: [
-| lconstr      (* ssrmatching plugin *)
-| "in" lconstr      (* ssrmatching plugin *)
-| lconstr "in" lconstr      (* ssrmatching plugin *)
-| "in" lconstr "in" lconstr      (* ssrmatching plugin *)
-| lconstr "in" lconstr "in" lconstr      (* ssrmatching plugin *)
-| lconstr "as" lconstr "in" lconstr      (* ssrmatching plugin *)
-]
-
-cpattern: [
-| "Qed" term      (* ssrmatching plugin *)
-| term      (* ssrmatching plugin *)
-]
-
-lcpattern: [
-| "Qed" lconstr      (* ssrmatching plugin *)
-| lconstr      (* ssrmatching plugin *)
-]
-
-ssrpatternarg: [
-| rpattern      (* ssrmatching plugin *)
-]
-
-empty: [
-|
-]
-
-lpar_id_coloneq: [
-| "(" IDENT; ":="
-]
-
-name_colon: [
-| IDENT; ":"
-| "_" ":"
-]
-
-int: [
-| integer
-]
-
-command_entry: [
-| noedit_mode
-]
-
diff --git a/doc/tools/docgram/prodn.edit_mlg b/doc/tools/docgram/prodn.edit_mlg
index a28d07636a..37197a1fec 100644
--- a/doc/tools/docgram/prodn.edit_mlg
+++ b/doc/tools/docgram/prodn.edit_mlg
@@ -12,3 +12,13 @@
 (* Contents used to generate prodn in doc *)
 
 DOC_GRAMMAR
+
+(* todo: doesn't work, gives
+ltac_match:  @match_key @ltac_expr with {? %| } {+| @ltac_expr } end
+instead of
+ltac_match:  @match_key @ltac_expr with {? %| } {+| {| @match_pattern | _ } => @ltac_expr } end
+
+SPLICE: [
+| match_rule
+]
+*)
diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg
index 84acd07075..42d94e76bb 100644
--- a/doc/tools/docgram/productionlist.edit_mlg
+++ b/doc/tools/docgram/productionlist.edit_mlg
@@ -15,11 +15,42 @@ DOC_GRAMMAR
 
 EXPAND: [ | ]
 
-(* ugh todo: try to handle before expansion *)
-tactic_then_gen : [
-| REPLACE ltac_expr_opt ".." ltac_expr_opt2
-| WITH ltac_expr_opt ".." or_opt ltac_expr_list2
+RENAME: [
+| name_alt names_tuple
+| binder_list binders
+| binder_list_opt binders_opt
+| typeclass_constraint_list_comma typeclass_constraints_comma
+| universe_expr_list_comma universe_exprs_comma
+| universe_level_list_opt universe_levels_opt
+| name_list names
+| name_list_comma names_comma
+| case_item_list_comma case_items_comma
+| eqn_list_or_opt eqns_or_opt
+| eqn_list_or eqns_or
+| pattern_list_or patterns_or
+| fix_body_list fix_bodies
+| arg_list args
+| arg_list_opt args_opt
+| evar_binding_list_semi evar_bindings_semi
 ]
 
-ltac_expr_opt2 : [ | DELETENT ]
-ltac_expr_list2_opt : [ | DELETENT ]
+binders_opt: [
+| REPLACE binders_opt binder
+| WITH binders
+]
+
+(* this is here because they're inside _opt generated by EXPAND *)
+SPLICE: [
+| ltac_info
+| eliminator
+| field_mods
+| ltac_production_sep
+| ltac_tactic_level
+| module_binder
+| printunivs_subgraph
+| quoted_attributes
+| ring_mods
+| scope_delimiter
+| univ_decl
+| univ_name_list
+]