Merge PR #11913: Doc_grammar: Update cmd:: and tacn:: constructs in .rsts

Reviewed-by: Zimmi48

8 files changed, 1077 insertions, 744 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 2abf6d02d2..8fcbeea570 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -996,7 +996,7 @@ are now available through the dot notation.
    Including multiple modules is a single :cmd:`Include` is equivalent to including each module
    in a separate :cmd:`Include` command.
 
-.. cmd:: Include Type @module_type_inl {* <+ @module_type_inl }
+.. cmd:: Include Type {+<+ @module_type_inl }
 
    .. deprecated:: 8.3
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 12a9a30f3d..fe359a23a9 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1533,10 +1533,8 @@ Computations
    | delta {? @delta_flag }
    ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums }
    | @one_term {? at @occs_nums }
-   occs_nums ::= {+ @num_or_var }
-   | - @num_or_var {* @int_or_var }
-   num_or_var ::= @num
-   | @ident
+   occs_nums ::= {+ {| @num | @ident } }
+   | - {| @num | @ident } {* @int_or_var }
    int_or_var ::= @int
    | @ident
    unfold_occ ::= @smart_qualid {? at @occs_nums }
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 8f325f957a..7ae98f4cd2 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -1,13 +1,13 @@
 # Grammar extraction tool for documentation
 
-`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and
-inserts it in chunks into `.rst` files.  The tool currently inserts
-Sphinx `productionlist` and `prodn` constructs (`productionlist` are
-gradually being replaced by `prodn` in the manual).  Updates to `tacn`
-and `cmd` constructs must be done manually since the grammar doesn't
-have names for them as it does for nonterminals.  There is an option
-to report which `tacn` and `cmd` were not found in the `.rst` files.
-`tacv` and `cmdv` constructs are not processed at all.
+`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it
+into `.rst` files.  The tool inserts `prodn` directives for  grammar productions.
+(`productionlist` are gradually being replaced by `prodn` in the manual.)
+It also updates `tacn` and `cmd` directives when they can be unambiguously matched to
+productions of the grammar (in practice, that's probably almost always).
+`tacv` and `cmdv` directives are not updated because matching them appears to require
+human judgement.  `doc_grammar` generates a few files that may be useful to
+developers and documentors.
 
 The mlg grammars present several challenges to generating an accurate grammar
 for documentation purposes:
@@ -34,46 +34,49 @@ for documentation purposes:
 
 ## What the tool does
 
-1. The tool reads all the `mlg` files and generates `fullGrammar`, which includes
-all the grammar without the actions for each production or the OCaml code.  This
-file is provided as a convenience to make it easier to examine the (mostly)
-unprocessed grammar of the mlg files with less clutter.  Nonterminals that use
-levels (`"5" RIGHTA` below) are modified, for example:
-
-```
-tactic_expr:
-  [ "5" RIGHTA
-    [ te = binder_tactic -> { te } ]
-```
-
-becomes
-
-```
-tactic_expr5: [
-| binder_tactic
-| tactic_expr4
-]
-```
-
-2. The tool applies grammar editing operations specified by `common.edit_mlg` to
-generate `editedGrammar`.
-
-3. `orderedGrammar` gives the desired order for the nonterminals and productions
-in the documented grammar.  Developers should edit this file to change the order.
-`doc_grammar` updates `orderedGrammar` so it has the same set of nonterminals and productions
-as `editedGrammar`.  The update process removes manually-added comments from
-`orderedGrammar` while automatically-generated comments will be regenerated.
-
-4. The tool applies further edits to the grammar specified by `productionlist.edit_mlg`,
-then it updates the productionlists in the `.rst` files as specified by comments in the form
-`.. insertgram <first nt> <last nt>`.  The edits are primarily to expand
-`.mlg` constructs such as `LIST1` and `OPT` into separate productions.  The tool
-generates `productionlistGrammar`, which has the entire grammar in the form of `productionlists`.
-
-5. Using the grammar produced in step 3, the tool applies edits specified by
-`prodn.edit_mlg` and generates `prodnGrammar`, representing each production as
-a Sphinx `prodn` construct.  Differently-edited grammars are used because `prodn`
-can naturally represent `LIST1 x SEP ','` whereas that is awkward for `productionlists`.
+1.  The tool reads all the `mlg` files and generates `fullGrammar`, which includes
+    all the grammar without the actions for each production or the OCaml code.  This
+    file is provided as a convenience to make it easier to examine the (mostly)
+    unprocessed grammar of the mlg files with less clutter.  Nonterminals that use
+    levels (`"5" RIGHTA` below) are modified, for example:
+
+    ```
+    tactic_expr:
+      [ "5" RIGHTA
+        [ te = binder_tactic -> { te } ]
+    ```
+
+    becomes
+
+    ```
+    tactic_expr5: [
+    | binder_tactic
+    | tactic_expr4
+    ]
+    ```
+
+2.  The tool applies grammar editing operations specified by `common.edit_mlg` to
+    generate `editedGrammar`.
+
+3. `orderedGrammar` gives the desired order for nonterminals and individual productions
+    in the documented grammar.  Developers should edit this file only to reorder lines.
+    `doc_grammar` updates `orderedGrammar` so it has the same set of nonterminals and productions
+    as `editedGrammar` while retaining the previous ordering.  Since the position of
+    new or renamed nonterminals is unspecified, they tend to show up in the wrong
+    place in `orderedGrammar`, therefore users should review the output and make
+    appropriate adjustments to the order.
+
+    The update process removes manually-added comments from `orderedGrammar` while
+    automatically-generated comments will be regenerated.
+
+4.  The tool updates the `.rst` files.  Comments in the form
+    `.. insertprodn <first nt> <last nt>` indicate inserting the productions for a
+    range of nonterminals.  `.. cmd::` and `.. tacn::` directives are updated using
+    prefixes in the form `[a-zA-Z0-9_ ]+` from the directive and the
+    grammar.  If there is unique match in the grammar, the directive is updated, if needed.
+    Multiple matches or no match gives an error message.
+
+5.  For reference, the tool generates `prodnGrammar`, which has the entire grammar in the form of `prodns`.
 
 ## How to use the tool
 
@@ -115,12 +118,12 @@ Other command line arguments:
 
 ### Grammar editing scripts
 
-The grammar editing scripts `*.edit_mlg` are similar in format to `.mlg` files stripped
+The grammar editing script `common.edit_mlg` is similar in format to `.mlg` files but stripped
 of all OCaml features.  This is an easy way to include productions to match or add without
 writing another parser.  The `DOC_GRAMMAR` token at the beginning of each file
-signals the use of streamlined syntax.
+signals the use of the streamlined syntax.
 
-Each edit file has a series of items in the form of productions.  Items are applied
+The edit file has a series of items in the form of productions.  Items are applied
 in the order they appear.  There are two types of editing operations:
 
 * Global edits - edit rules that apply to the entire grammar in a single operation.
@@ -137,7 +140,7 @@ such as `empty: [ | ]`, which adds a new non-terminal `empty` with an
 empty production on the right-hand side.
 
 Another example: `LEFTQMARK: [ | "?" ]` is a local edit that treats `LEFTQMARK` as
-the name of a non-terminal and adds one production for it.  (We know that LEFTQMARK
+the name of a non-terminal and adds a production for it.  (We know that LEFTQMARK
 is a token but doc_grammar does not.)  `SPLICE: [ | LEFTQMARK ]` requests replacing all
 uses of `LEFTQMARK` anywhere in the grammar with its productions and removing the
 non-terminal.  The combined effect of these two is to replace all uses of
@@ -192,7 +195,7 @@ that appear in the specified production:
 ```
 
 `MOVETO <destination> <production>` - moves the production to `<destination>` and,
- if needed, creates a new production <edited_nt> -> <destination>.
+ if needed, creates a new production <edited_nt> -> \<destination>.
 
 `OPTINREF` - verifies that <edited_nt> has an empty production.  If so, it removes
 the empty production and replaces all references to <edited_nt> throughout the
@@ -201,7 +204,7 @@ grammar with `OPT <edited_nt>`
 `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)
+`(any other nonterminal name)` - adds a new production (and possibly a new nonterminal)
 to the grammar.
 
 ### `.rst` file updates
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 541717581c..88a5217652 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -536,6 +536,13 @@ gallina_ext: [
 | REPLACE "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ]
 | WITH "Generalizable" [  [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ]
 
+| REPLACE "Export" "Set" option_table option_setting
+| WITH OPT "Export" "Set" option_table option_setting
+| REPLACE "Export" "Unset" option_table
+| WITH OPT "Export" "Unset" option_table
+| REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
+| WITH "Instance" instance_name ":" operconstr200 hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ]
+
 ]
 
 (* lexer stuff *)
@@ -658,6 +665,19 @@ selector_body: [
 
 range_selector_or_nth: [ | DELETENT ]
 
+firstorder_rhs: [
+| firstorder_using
+| "with" LIST1 preident
+| firstorder_using "with" LIST1 preident
+]
+
+where: [
+| "at" "top"
+| "at" "bottom"
+| "after" ident
+| "before" ident
+]
+
 simple_tactic: [
 | DELETE "intros"
 | REPLACE "intros" ne_intropatterns
@@ -665,6 +685,158 @@ simple_tactic: [
 | DELETE "eintros"
 | REPLACE "eintros" ne_intropatterns
 | WITH "eintros" intropatterns
+| DELETE "autorewrite" "with" LIST1 preident clause
+| DELETE "autorewrite" "with" LIST1 preident clause "using" tactic
+| DELETE "autorewrite" "*" "with" LIST1 preident clause
+| REPLACE "autorewrite" "*" "with" LIST1 preident clause "using" tactic
+| WITH "autorewrite" OPT "*" "with" LIST1 preident clause_dft_concl OPT ( "using" tactic )
+| DELETE "cofix" ident
+| REPLACE "cofix" ident "with" LIST1 cofixdecl
+| WITH "cofix" ident OPT ( "with" LIST1 cofixdecl )
+| DELETE "constructor"
+| DELETE "constructor" int_or_var
+| REPLACE "constructor" int_or_var "with" bindings
+| WITH "constructor" OPT int_or_var OPT ( "with" bindings )
+| DELETE "econstructor"
+| DELETE "econstructor" int_or_var
+| REPLACE "econstructor" int_or_var "with" bindings
+| WITH "econstructor" OPT ( int_or_var OPT ( "with" bindings ) )
+| DELETE "dependent" "rewrite" orient constr
+| REPLACE "dependent" "rewrite" orient constr "in" hyp
+| WITH "dependent" "rewrite" orient constr OPT ( "in" hyp )
+| "firstorder" OPT tactic firstorder_rhs
+| DELETE "firstorder" OPT tactic firstorder_using
+| DELETE "firstorder" OPT tactic "with" LIST1 preident
+| DELETE "firstorder" OPT tactic firstorder_using "with" LIST1 preident
+| DELETE "fix" ident natural
+| REPLACE "fix" ident natural "with" LIST1 fixdecl
+| WITH "fix" ident natural OPT ( "with" LIST1 fixdecl )
+| DELETE "generalize" constr
+| REPLACE "generalize" constr LIST1 constr
+| WITH "generalize" constr OPT ( LIST1 constr )
+| EDIT "simplify_eq" ADD_OPT destruction_arg
+| EDIT "esimplify_eq" ADD_OPT destruction_arg
+| EDIT "discriminate" ADD_OPT destruction_arg
+| EDIT "ediscriminate" ADD_OPT destruction_arg
+| DELETE "injection"
+| DELETE "injection" destruction_arg
+| DELETE "injection" "as" LIST0 simple_intropattern
+| REPLACE "injection" destruction_arg "as" LIST0 simple_intropattern
+| WITH "injection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern )
+| DELETE "einjection"
+| DELETE "einjection" destruction_arg
+| DELETE "einjection" "as" LIST0 simple_intropattern
+| REPLACE "einjection" destruction_arg "as" LIST0 simple_intropattern
+| WITH "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern )
+| EDIT "simple" "injection" ADD_OPT destruction_arg
+| DELETE "intro"  (* todo: change the mlg to simplify! *)
+| DELETE "intro" ident
+| DELETE "intro" ident "at" "top"
+| DELETE "intro" ident "at" "bottom"
+| DELETE "intro" ident "after" hyp
+| DELETE "intro" ident "before" hyp
+| DELETE "intro" "at" "top"
+| DELETE "intro" "at" "bottom"
+| DELETE "intro" "after" hyp
+| DELETE "intro" "before" hyp
+| "intro" OPT ident OPT where
+| DELETE "move" hyp "at" "top"
+| DELETE "move" hyp "at" "bottom"
+| DELETE "move" hyp "after" hyp
+| DELETE "move" hyp "before" hyp
+| "move" ident OPT where
+| DELETE "replace" "->" uconstr clause
+| DELETE "replace" "<-" uconstr clause
+| DELETE "replace" uconstr clause
+| "replace" orient uconstr clause_dft_concl   (* todo: fix 'clause' *)
+| REPLACE "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac
+| WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences by_arg_tac )
+| DELETE "rewrite" "*" orient uconstr "in" hyp by_arg_tac
+| DELETE "rewrite" "*" orient uconstr "at" occurrences by_arg_tac
+| DELETE "rewrite" "*" orient uconstr by_arg_tac
+| DELETE "setoid_rewrite" orient glob_constr_with_bindings
+| DELETE "setoid_rewrite" orient glob_constr_with_bindings "in" hyp
+| DELETE "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences
+| REPLACE "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" hyp
+| WITH "setoid_rewrite" orient glob_constr_with_bindings OPT ( "at" occurrences ) OPT ( "in" hyp )
+| REPLACE "stepl" constr "by" tactic
+| WITH "stepl" constr OPT ( "by" tactic )
+| DELETE "stepl" constr
+| REPLACE "stepr" constr "by" tactic
+| WITH "stepr" constr OPT ( "by" tactic )
+| DELETE "stepr" constr
+| DELETE "unify" constr constr
+| REPLACE "unify" constr constr "with" preident
+| WITH "unify" constr constr OPT ( "with" preident )
+| DELETE "cutrewrite" orient constr
+| REPLACE "cutrewrite" orient constr "in" hyp
+| WITH "cutrewrite" orient constr OPT ( "in" hyp )
+| DELETE "destauto"
+| REPLACE "destauto" "in" hyp
+| WITH "destauto" OPT ( "in" hyp )
+| REPLACE "autounfold_one" hintbases "in" hyp
+| WITH "autounfold_one" hintbases OPT ( "in" hyp )
+| DELETE "autounfold_one" hintbases
+| REPLACE "rewrite_db" preident "in" hyp
+| WITH "rewrite_db" preident OPT ( "in" hyp )
+| DELETE "rewrite_db" preident
+| DELETE "setoid_symmetry"
+| REPLACE "setoid_symmetry" "in" hyp
+| WITH "setoid_symmetry" OPT ( "in" hyp )
+| REPLACE "rewrite_strat" rewstrategy "in" hyp
+| WITH "rewrite_strat" rewstrategy OPT ( "in" hyp )
+| DELETE "rewrite_strat" rewstrategy
+| REPLACE "protect_fv" string "in" ident
+| WITH "protect_fv" string OPT ( "in" ident )
+| DELETE "protect_fv" string
+| DELETE "symmetry"
+| REPLACE "symmetry" "in" in_clause
+| WITH "symmetry" OPT ( "in" in_clause )
+| DELETE "split"
+| REPLACE "split" "with" bindings
+| WITH  "split" OPT ( "with" bindings )
+| DELETE "esplit"
+| REPLACE "esplit" "with" bindings
+| WITH "esplit" OPT ( "with" bindings )
+| DELETE "specialize" constr_with_bindings
+| REPLACE "specialize" constr_with_bindings "as" simple_intropattern
+| WITH "specialize" constr_with_bindings OPT ( "as" simple_intropattern )
+| DELETE "exists"
+| REPLACE "exists" LIST1 bindings SEP ","
+| WITH "exists" OPT ( LIST1 bindings SEP "," )
+| DELETE "eexists"
+| REPLACE "eexists" LIST1 bindings SEP ","
+| WITH "eexists" OPT ( LIST1 bindings SEP "," )
+| DELETE "left"
+| REPLACE "left" "with" bindings
+| WITH "left" OPT ( "with" bindings )
+| DELETE "eleft"
+| REPLACE "eleft" "with" bindings
+| WITH "eleft" OPT ( "with" bindings )
+| DELETE "right"
+| REPLACE "right" "with" bindings
+| WITH "right" OPT ( "with" bindings )
+| DELETE "eright"
+| REPLACE "eright" "with" bindings
+| WITH "eright" OPT ( "with" bindings )
+| DELETE "finish_timing" OPT string
+| REPLACE "finish_timing" "(" string ")" OPT string
+| WITH "finish_timing" OPT ( "(" string ")" ) OPT string
+| REPLACE "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr
+| WITH "hresolve_core" "(" ident ":=" constr ")" OPT ( "at" int_or_var ) "in" constr
+| DELETE "hresolve_core" "(" ident ":=" constr ")" "in" constr
+| EDIT "psatz_R" ADD_OPT int_or_var tactic
+| EDIT "psatz_Q" ADD_OPT int_or_var tactic
+| EDIT "psatz_Z" ADD_OPT int_or_var tactic
+| REPLACE "subst" LIST1 var
+| WITH "subst" OPT ( LIST1 var )
+| DELETE "subst"
+| DELETE "congruence"
+| DELETE "congruence" int
+| DELETE "congruence" "with" LIST1 constr
+| REPLACE "congruence" int "with" LIST1 constr
+| WITH "congruence" OPT int OPT ( "with" LIST1 constr )
+
 ]
 
 (* todo: don't use DELETENT for this *)
@@ -700,6 +872,110 @@ command: [
 | WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc )      (* funind plugin *)
 | REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
 | WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )      (* funind plugin *)
+| DELETE "Cd"
+| REPLACE "Cd" ne_string
+| WITH "Cd" OPT ne_string
+| DELETE "Back"
+| REPLACE "Back" natural
+| WITH "Back" OPT natural
+| REPLACE "Test" option_table "for" LIST1 option_ref_value
+| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value )
+| DELETE "Test" option_table
+| REPLACE "Load" [ "Verbose" | ] [ ne_string | IDENT ]
+| WITH "Load" OPT "Verbose" [ ne_string | IDENT ]
+| DELETE "Unset" option_table
+| DELETE "Set" option_table option_setting
+| REPLACE "Add" IDENT IDENT LIST1 option_ref_value
+| WITH "Add" IDENT OPT IDENT LIST1 option_ref_value
+| DELETE "Add" IDENT LIST1 option_ref_value
+| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
+| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident
+| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" ident
+| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" ident
+| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "as" ident
+| "Add" "Parametric" "Relation" binders ":" constr constr OPT ( "reflexivity" "proved" "by" constr ) OPT ( "symmetry" "proved" "by" constr ) OPT ("transitivity" "proved" "by" constr ) "as" ident
+| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
+| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "as" ident
+| DELETE "Add" "Relation" constr constr "as" ident
+| DELETE "Add" "Relation" constr constr "symmetry" "proved" "by" constr "as" ident
+| DELETE "Add" "Relation" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| DELETE "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Relation" constr constr OPT ( "reflexivity" "proved" "by" constr ) OPT ( "symmetry" "proved" "by" constr ) OPT ( "transitivity" "proved" "by" constr ) "as" ident
+| REPLACE "Admit" "Obligations" "of" ident
+| WITH "Admit" "Obligations" OPT ( "of" ident )
+| DELETE "Admit" "Obligations"
+| REPLACE "Create" "HintDb" IDENT; [ "discriminated" | ]
+| WITH "Create" "HintDb" IDENT; OPT "discriminated"
+| DELETE "Debug" "On"
+| REPLACE "Debug" "Off"
+| WITH "Debug" [ "On" | "Off" ]
+| EDIT "Defined" ADD_OPT identref
+| REPLACE "Derive" "Inversion" ident "with" constr "Sort" sort_family
+| WITH "Derive" "Inversion" ident "with" constr OPT ( "Sort" sort_family )
+| DELETE "Derive" "Inversion" ident "with" constr
+| REPLACE "Derive" "Inversion_clear" ident "with" constr "Sort" sort_family
+| WITH "Derive" "Inversion_clear" ident "with" constr OPT ( "Sort" sort_family )
+| DELETE "Derive" "Inversion_clear" ident "with" constr
+| EDIT "Focus" ADD_OPT natural
+| DELETE "Hint" "Rewrite" orient LIST1 constr ":" LIST0 preident
+| REPLACE "Hint" "Rewrite" orient LIST1 constr "using" tactic ":" LIST0 preident
+| WITH "Hint" "Rewrite" orient LIST1 constr OPT ( "using" tactic ) OPT ( ":" LIST0 preident )
+| DELETE "Hint" "Rewrite" orient LIST1 constr
+| DELETE "Hint" "Rewrite" orient LIST1 constr "using" tactic
+| REPLACE "Next" "Obligation" "of" ident withtac
+| WITH "Next" "Obligation" OPT ( "of" ident ) withtac
+| DELETE "Next" "Obligation" withtac
+| REPLACE "Obligation" int "of" ident ":" lglob withtac
+| WITH "Obligation" int OPT ( "of" ident ) OPT ( ":" lglob withtac )
+| DELETE "Obligation" int "of" ident withtac
+| DELETE "Obligation" int ":" lglob withtac
+| DELETE "Obligation" int withtac
+| REPLACE "Obligations" "of" ident
+| WITH "Obligations" OPT ( "of" ident )
+| DELETE "Obligations"
+| REPLACE "Preterm" "of" ident
+| WITH "Preterm" OPT ( "of" ident )
+| DELETE "Preterm"
+| EDIT "Remove" ADD_OPT IDENT IDENT LIST1 option_ref_value
+| DELETE "Restore" "State" IDENT
+| DELETE "Restore" "State" ne_string
+| "Restore" "State" [ IDENT | ne_string ]
+| DELETE "Show"
+| DELETE "Show" natural
+| DELETE "Show" ident
+| "Show" OPT [ ident | natural ]
+| DELETE "Show" "Ltac" "Profile"
+| REPLACE "Show" "Ltac" "Profile" "CutOff" int
+| WITH "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ]
+| DELETE "Show" "Ltac" "Profile" string
+| DELETE "Show" "Proof"  (* combined with Show Proof Diffs in vernac_toplevel *)
+| REPLACE "Solve" "All" "Obligations" "with" tactic
+| WITH "Solve" "All" "Obligations" OPT ( "with" tactic )
+| DELETE "Solve" "All" "Obligations"
+| REPLACE "Solve" "Obligation" int "of" ident "with" tactic
+| WITH "Solve" "Obligation" int OPT ( "of" ident ) "with" tactic
+| DELETE "Solve" "Obligations"
+| DELETE "Solve" "Obligation" int "with" tactic
+| REPLACE "Solve" "Obligations" "of" ident "with" tactic
+| WITH "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" tactic )
+| DELETE "Solve" "Obligations" "with" tactic
+| DELETE "Undo"
+| DELETE "Undo" natural
+| REPLACE "Undo" "To" natural
+| WITH "Undo" OPT ( OPT "To" natural )
+| DELETE "Write" "State" IDENT
+| REPLACE "Write" "State" ne_string
+| WITH "Write" "State" [ IDENT | ne_string ]
+| DELETE "Abort"
+| DELETE "Abort" "All"
+| REPLACE "Abort" identref
+| WITH "Abort" OPT [ "All" | identref ]
+
 ]
 
 only_parsing: [
@@ -828,11 +1104,221 @@ record_binder: [
 | DELETE name
 ]
 
+at_level_opt: [
+| OPTINREF
+]
+
+query_command: [
+| REPLACE "Eval" red_expr "in" lconstr "."
+| WITH "Eval" red_expr "in" lconstr
+| REPLACE "Compute" lconstr "."
+| WITH "Compute" lconstr
+| REPLACE "Check" lconstr "."
+| WITH "Check" lconstr
+| REPLACE "About" smart_global OPT univ_name_list "."
+| WITH "About" smart_global OPT univ_name_list
+| REPLACE "SearchHead" constr_pattern in_or_out_modules "."
+| WITH "SearchHead" constr_pattern in_or_out_modules
+| REPLACE "SearchPattern" constr_pattern in_or_out_modules "."
+| WITH "SearchPattern" constr_pattern in_or_out_modules
+| REPLACE "SearchRewrite" constr_pattern in_or_out_modules "."
+| WITH "SearchRewrite" constr_pattern in_or_out_modules
+| REPLACE "Search" searchabout_query searchabout_queries "."
+| WITH "Search" searchabout_query searchabout_queries
+| REPLACE "SearchAbout" searchabout_query searchabout_queries "."
+| WITH "SearchAbout" searchabout_query searchabout_queries
+| REPLACE "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
+| WITH "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules
+]
+
+vernac_toplevel: [
+(* note these commands can't be referenced by vernac_control commands *)
+| REPLACE "Drop" "."
+| WITH "Drop"
+| REPLACE "Quit" "."
+| WITH "Quit"
+| REPLACE "BackTo" natural "."
+| WITH "BackTo" natural
+| REPLACE "Show" "Goal" natural "at" natural "."
+| WITH "Show" "Goal" natural "at" natural
+| REPLACE "Show" "Proof" "Diffs" OPT "removed" "."
+| WITH "Show" "Proof" OPT ( "Diffs" OPT "removed" )
+| DELETE vernac_control
+]
+
+positive_search_mark: [
+| OPTINREF
+]
+
+in_or_out_modules: [
+| OPTINREF
+]
+
+searchabout_queries: [
+| OPTINREF
+]
+
+vernac_control: [
+(* replacing vernac_control with command is cheating a little;
+   they can't refer to the vernac_toplevel commands.
+   cover this the descriptions of these commands *)
+| REPLACE "Time" vernac_control
+| WITH "Time" command
+| REPLACE "Redirect" ne_string vernac_control
+| WITH "Redirect" ne_string command
+| REPLACE "Timeout" natural vernac_control
+| WITH "Timeout" natural command
+| REPLACE "Fail" vernac_control
+| WITH "Fail" command
+| DELETE decorated_vernac
+]
+
+option_setting: [
+| OPTINREF
+]
+
+orient: [
+| OPTINREF
+]
+
+in_hyp_as: [
+| OPTINREF
+]
+
+as_name: [
+| OPTINREF
+]
+
+hloc: [
+| OPTINREF
+]
+
+as_or_and_ipat: [
+| OPTINREF
+]
+
+hintbases: [
+| OPTINREF
+]
+
+as_ipat: [
+| OPTINREF
+]
+
+auto_using: [
+| OPTINREF
+]
+
+with_bindings: [
+| OPTINREF
+]
+
+eqn_ipat: [
+| OPTINREF
+]
+
+withtac: [
+| OPTINREF
+]
+
 of_module_type: [
 | (* empty *)
 | OPTINREF
 ]
 
+
+clause_dft_all: [
+| OPTINREF
+]
+
+opt_clause: [
+| OPTINREF
+]
+
+with_names: [
+| OPTINREF
+]
+
+in_hyp_list: [
+| OPTINREF
+]
+
+struct_annot: [
+| OPTINREF
+]
+
+firstorder_using: [
+| OPTINREF
+]
+
+fun_ind_using: [
+| OPTINREF
+]
+
+by_arg_tac: [
+| OPTINREF
+]
+
+by_tactic: [
+| OPTINREF
+]
+
+rewriter: [
+| REPLACE [ "?" | LEFTQMARK ] constr_with_bindings_arg
+| WITH "?" constr_with_bindings_arg
+]
+
+intropattern_or_list_or: [
+(* todo: where does intropattern_or_list_or come from?? *)
+| REPLACE intropattern_or_list_or "|" intropatterns
+| WITH LIST0 intropattern LIST0 ( "|" intropatterns )
+| DELETE intropatterns
+]
+
+record_declaration: [
+| DELETE fields_def
+| LIST0 field_def
+]
+
+fields_def: [ | DELETENT ]
+
+hint_info: [
+| OPTINREF
+]
+
+debug: [
+| OPTINREF
+]
+
+eauto_search_strategy: [
+| OPTINREF
+]
+
+
+constr_body: [
+| DELETE ":=" lconstr
+| REPLACE ":" lconstr ":=" lconstr
+| WITH OPT ( ":" lconstr ) ":=" lconstr
+]
+
+opt_hintbases: [
+| OPTINREF
+]
+
+opthints: [
+| OPTINREF
+]
+
+scheme: [
+| DELETE scheme_kind
+| REPLACE identref ":=" scheme_kind
+| WITH OPT ( identref ":=" ) scheme_kind
+]
+
+instance_name: [
+| OPTINREF
+]
+
 simple_reserv: [
 | REPLACE LIST1 identref ":" lconstr
 | WITH LIST1 identref ":" type
@@ -871,7 +1357,6 @@ module_expr: [
 
 SPLICE: [
 | noedit_mode
-| command_entry
 | bigint
 | match_list
 | match_context_list
@@ -975,7 +1460,6 @@ SPLICE: [
 | binders_fixannot
 | as_return_type
 | case_type
-| fields_def
 | universe_increment
 | type_cstr
 | record_pattern
@@ -1002,6 +1486,20 @@ SPLICE: [
 | record_fields
 | constructor_type
 | record_binder
+| at_level_opt
+| option_ref_value
+| positive_search_mark
+| in_or_out_modules
+| register_prim_token
+| option_setting
+| orient
+| with_bindings
+| by_arg_tac
+| by_tactic
+| quantified_hypothesis
+| nat_or_var
+| in_hyp_list
+| rename
 | export_token
 | reserv_tuple
 | inst
@@ -1010,6 +1508,20 @@ SPLICE: [
 | is_module_type
 | is_module_expr
 | module_expr
+| mlname
+| withtac
+| debug
+| eauto_search_strategy
+| constr_body
+| reference_or_constr
+| opt_hintbases
+| hints_path_atom
+| opthints
+| scheme
+| fresh_id
+| ltac_def_kind
+| intropatterns
+| instance_name
 ] (* end SPLICE *)
 
 RENAME: [
@@ -1026,7 +1538,6 @@ RENAME: [
 | tactic_expr0 ltac_expr0
 
 (* | nonsimple_intropattern intropattern (* ltac2 *) *)
-| intropatterns intropattern_list_opt
 
 | operconstr200 term   (* historical name *)
 | operconstr100 term100
@@ -1045,7 +1556,6 @@ RENAME: [
 | match_hyps match_hyp
 
 | BULLET bullet
-| nat_or_var num_or_var
 | fix_decl fix_body
 | cofix_decl cofix_body
 | constr one_term
@@ -1063,5 +1573,90 @@ RENAME: [
 | smart_global smart_qualid
 ]
 
+(* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *)
+clause_dft_concl: [
+| OPTINREF
+]
+
+(* add in ltac and Tactic Notation tactics that appear in the doc: *)
+ltac_defined_tactics: [
+| "classical_left"
+| "classical_right"
+| "contradict" ident
+| "discrR"
+| "easy"
+| "exfalso"
+| "inversion_sigma"
+| "lia"
+| "lra"
+| "nia"
+| "nra"
+| "split_Rabs"
+| "split_Rmult"
+| "tauto"
+| "zify"
+]
+
+(* todo: need careful review; assume that "[" ... "]" are literals *)
+tactic_notation_tactics: [
+| "assert_fails" ltac_expr3
+| "assert_succeeds" ltac_expr3
+| "field" OPT ( "[" LIST1 term "]" )
+| "field_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
+| "field_simplify_eq" OPT ( "[" LIST1 term "]" ) OPT ( "in" ident )
+| "intuition" OPT ltac_expr
+| "nsatz" OPT ( "with" "radicalmax" ":=" term "strategy" ":=" term "parameters" ":=" term "variables" ":=" term )
+| "psatz" term OPT int_or_var
+| "ring" OPT ( "[" LIST1 term "]" )
+| "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )  (* todo: ident was "hyp", worth keeping? *)
+]
+
+tacticals: [
+]
+
+simple_tactic: [
+| ltac_defined_tactics
+| tactic_notation_tactics
+]
+
+(* move all commands under "command" *)
+
+DELETE: [
+| vernac
+]
 
+tactic_mode: [
+(* todo: make sure to document this production! *)
+(* deleting to allow splicing query_command into command *)
+| DELETE OPT toplevel_selector query_command
+]
+
+vernac_aux: [
+| DELETE gallina "."
+| DELETE gallina_ext "."
+| DELETE syntax "."
+| DELETE command_entry
+]
+
+command: [
+| gallina
+| gallina_ext
+| syntax
+| query_command
+| vernac_control
+| vernac_toplevel
+| command_entry
+]
+
+SPLICE: [
+| gallina
+| gallina_ext
+| syntax
+| query_command
+| vernac_control
+| vernac_toplevel
+| command_entry
+| ltac_defined_tactics
+| tactic_notation_tactics
+]
 (* 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 5c9a13668f..0450aee2ec 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -48,7 +48,7 @@ let default_args = {
   verify = false;
 }
 
-let start_symbols = ["vernac_toplevel"]
+let start_symbols = ["vernacular"]
 let tokens = [ "bullet"; "string"; "unicode_id_part"; "unicode_letter" ]
 
 (* translated symbols *)
@@ -1165,7 +1165,7 @@ let apply_edit_file g edits =
             in
             aux tl prods' add_nt
           | (Snterm "OPTINREF" :: _) :: tl ->
-            if not (List.mem [] prods) then
+            if not (has_match [] prods) then
               error "OPTINREF but no empty production for %s\n" nt;
             global_repl g [(Snterm nt)] [(Sopt (Snterm nt))];
             aux tl (remove_prod [] prods nt) add_nt
@@ -1618,8 +1618,11 @@ let finish_with_file old_file verify =
 let open_temp_bin file =
   open_out_bin (sprintf "%s_temp" file)
 
+let match_cmd_regex = Str.regexp "[a-zA-Z0-9_ ]+"
+
 let find_longest_match prods str =
-  (* todo: require a minimum length? *)
+  let get_pfx str = String.trim (if Str.string_match match_cmd_regex str 0 then Str.matched_string str else "") in
+  let prods = StringSet.fold (fun a lst -> a :: lst) prods [] in  (* todo: wasteful! *)
   let common_prefix_len s1 s2 =
     let limit = min (String.length s1) (String.length s2) in
     let rec aux off =
@@ -1631,13 +1634,16 @@ let find_longest_match prods str =
   in
 
   let slen = String.length str in
+  let str_pfx = get_pfx str in
   let rec longest best multi best_len prods =
     match prods with
     | [] -> best, multi, best_len
     | prod :: tl ->
-      let pstr = String.trim (prod_to_prodn prod) in
+      let pstr = String.trim prod in  (* todo: should be pretrimmed *)
       let clen = common_prefix_len str pstr in
-      if clen = slen && slen = String.length pstr then
+      if str_pfx = "" || str_pfx <> get_pfx pstr then
+        longest best multi best_len tl  (* prefixes don't match *)
+      else if clen = slen && slen = String.length pstr then
         pstr, false, clen  (* exact match *)
       else if clen > best_len then
         longest pstr false clen tl  (* better match *)
@@ -1651,6 +1657,7 @@ let find_longest_match prods str =
 type seen = {
   nts: (string * int) NTMap.t;
   tacs: (string * int) NTMap.t;
+  tacvs: (string * int) NTMap.t;
   cmds: (string * int) NTMap.t;
   cmdvs: (string * int) NTMap.t;
 }
@@ -1659,8 +1666,9 @@ let process_rst g file args seen tac_prods cmd_prods =
   let old_rst = open_in file in
   let new_rst = open_temp_bin file in
   let linenum = ref 0 in
-  let dir_regex = Str.regexp "^\\([ \t]*\\)\\.\\.[ \t]*\\([a-zA-Z0-9:]*\\)\\(.*\\)" in
-  let ig_args_regex = Str.regexp "^[ \t]*\\([a-zA-Z0-9_\\.]*\\)[ \t]*\\([a-zA-Z0-9_\\.]*\\)" in
+  let dir_regex = Str.regexp "^\\([ \t]*\\)\\.\\.[ \t]*\\([a-zA-Z0-9:]* *\\)\\(.*\\)" in
+  let contin_regex = Str.regexp "^\\([ \t]*\\)\\(.*\\)" in
+  let ip_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 getline () =
@@ -1692,7 +1700,7 @@ let process_rst g file args seen tac_prods cmd_prods =
   in
 
   let process_insertprodn line rhs =
-    if not (Str.string_match ig_args_regex rhs 0) then
+    if not (Str.string_match ip_args_regex rhs 0) then
       error "%s line %d: bad arguments '%s' for 'insertprodn'\n" file !linenum rhs
     else begin
       let start = Str.matched_group 1 rhs in
@@ -1703,8 +1711,8 @@ let process_rst g file args seen tac_prods cmd_prods =
         error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum start;
       if end_index = None then
         error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum end_;
-      if start_index <> None && end_index <> None then
-        check_range_consistency g start 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
@@ -1716,7 +1724,7 @@ let process_rst g file args seen tac_prods cmd_prods =
               error "%s line %d: expecting a blank line after 'insertprodn'\n" file !linenum
             else begin
               let line3 = getline() in
-              if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "prodn::" then
+              if not (Str.string_match dir_regex line3 0) || (String.trim (Str.matched_group 2 line3)) <> "prodn::" then
                 error "%s line %d: expecting '.. prodn::' after 'insertprodn'\n" file !linenum
               else begin
                 let indent = Str.matched_group 1 line3 in
@@ -1736,38 +1744,82 @@ let process_rst g file args seen tac_prods cmd_prods =
         end
       | _ -> ()
     end
+  in
+
+(*  let skip_files = ["doc/sphinx/proof-engine/ltac.rst"; "doc/sphinx/proof-engine/ltac2.rst";*)
+(*    "doc/sphinx/proof-engine/ssreflect-proof-language.rst"]*)
+(*  in*)
 
+  let cmd_replace_files = [
+    "doc/sphinx/language/gallina-specification-language.rst";
+    "doc/sphinx/language/gallina-extensions.rst"
+  ]
   in
+
+  let save_n_get_more direc pfx first_rhs seen_map prods =
+    let replace rhs prods =
+      if StringSet.is_empty prods || not (List.mem file cmd_replace_files) then
+        rhs (* no change *)
+      else
+        let mtch, multi, len = find_longest_match prods rhs in
+        if mtch = rhs then
+          rhs (* no change *)
+        else if mtch = "" then begin
+          warn "%s line %d: NO MATCH `%s`\n" file !linenum rhs;
+          rhs
+        end else if multi then begin
+          warn "%s line %d: MULTIMATCH `%s`\n" file !linenum rhs;
+          rhs
+        end else
+          mtch (* update cmd/tacn *)
+    in
+    let map = ref seen_map in
+    if NTMap.mem first_rhs !map then
+      warn "%s line %d: Repeated %s: '%s'\n" file !linenum direc first_rhs;
+(*    if not (StringSet.mem rhs seen_map) then*)
+(*      warn "%s line %d: Unknown tactic: '%s'\n" file !linenum rhs;*)
+
+    fprintf new_rst "%s%s\n" pfx (replace first_rhs prods);
+
+    map := NTMap.add first_rhs (file, !linenum) !map;
+    while
+      let nextline = getline() in
+      ignore (Str.string_match contin_regex nextline 0);
+      let indent = Str.matched_group 1 nextline in
+      let rhs = Str.matched_group 2 nextline in
+      let replaceable = rhs <> "" && rhs.[0] <> ':' in
+      let upd_rhs = if replaceable then (replace rhs prods) else rhs in
+      fprintf new_rst "%s%s\n" indent upd_rhs;
+      if replaceable then begin
+        map := NTMap.add rhs (file, !linenum) !map
+      end;
+      rhs <> ""
+    do
+      ()
+    done;
+    !map
+  in
+
   try
     while true do
       let line = getline() in
       if Str.string_match dir_regex line 0 then begin
-        let dir = Str.matched_group 2 line in
-        let rhs = String.trim (Str.matched_group 3 line) in
+        let dir = String.trim (Str.matched_group 2 line) in
+        let rhs = Str.matched_group 3 line in
+        let pfx = String.sub line 0 (Str.group_end 2) in
         match dir with
         | "prodn::" ->
           if rhs = "coq" then
             warn "%s line %d: Missing 'insertprodn' before 'prodn:: coq'\n" file !linenum;
           fprintf new_rst "%s\n" line;
         | "tacn::" when args.check_tacs ->
-          if not (StringSet.mem rhs tac_prods) then
-            warn "%s line %d: Unknown tactic: '%s'\n" file !linenum rhs;
-          if NTMap.mem rhs !seen.tacs then
-            warn "%s line %d: Repeated tactic: '%s'\n" file !linenum rhs;
-          seen := { !seen with tacs = (NTMap.add rhs (file, !linenum) !seen.tacs)};
-          fprintf new_rst "%s\n" line
+          seen := { !seen with tacs = save_n_get_more "tacn" pfx rhs !seen.tacs tac_prods }
+        | "tacv::" when args.check_tacs ->
+          seen := { !seen with tacvs = save_n_get_more "tacv" pfx rhs !seen.tacvs StringSet.empty }
         | "cmd::" when args.check_cmds ->
-(*
-          if not (StringSet.mem rhs cmd_prods) then
-            warn "%s line %d: Unknown command: '%s'\n" file !linenum rhs;
-          if NTMap.mem rhs !seen.cmds then
-            warn "%s line %d: Repeated command: '%s'\n" file !linenum rhs;
-*)
-          seen := { !seen with cmds = (NTMap.add rhs (file, !linenum) !seen.cmds)};
-          fprintf new_rst "%s\n" line
+          seen := { !seen with cmds = save_n_get_more "cmd" pfx rhs !seen.cmds cmd_prods }
         | "cmdv::" when args.check_cmds ->
-          seen := { !seen with cmdvs = (NTMap.add rhs (file, !linenum) !seen.cmdvs)};
-          fprintf new_rst "%s\n" line
+          seen := { !seen with cmdvs = save_n_get_more "cmdv" pfx rhs !seen.cmdvs StringSet.empty }
         | "insertprodn" ->
           process_insertprodn line rhs
         | _ -> fprintf new_rst "%s\n" line
@@ -1835,19 +1887,7 @@ let process_grammar args =
       let common_edits = read_mlg_edit "common.edit_mlg" in
       apply_edit_file g common_edits
     end;
-    let prodn_gram = ref { map = !g.map; order = !g.order } in
-
-    if !exit_code = 0 && not args.verify then begin
-      let prodlist_edits = read_mlg_edit "productionlist.edit_mlg" in
-      apply_edit_file g prodlist_edits;
-      let out = open_temp_bin (dir "productionlistGrammar") in
-      if args.verbose then
-        report_info g !symdef_map;
-      print_in_order out g `PRODLIST !g.order StringSet.empty;
-      (*print_chunks g out `PRODLIST ();*)
-      close_out out;
-      finish_with_file (dir "productionlistGrammar") args.verify;
-    end;
+    let prodn_gram = ref { map = !g.map; order = !g.order } in  (* todo: should just be 'g', right? *)
 
     if !exit_code = 0 && not args.verify then begin
       let out = open_temp_bin (dir "editedGrammar") in
@@ -1864,7 +1904,7 @@ let process_grammar args =
       let ordered_grammar = read_mlg_edit "orderedGrammar" in
       let out = open_temp_bin (dir "orderedGrammar") in
       fprintf out "%s\n%s\n\n"
-          ("(* Defines the order to apply to editedGrammar to get productionlistGrammar.\n" ^
+          ("(* Defines the order to apply to editedGrammar to get the final grammar for the doc.\n" ^
           "doc_grammar will modify this file to add/remove nonterminals and productions\n" ^
            "to match editedGrammar, which will remove comments.  Not compiled into Coq *)")
           "DOC_GRAMMAR";
@@ -1883,7 +1923,7 @@ let process_grammar args =
         list, StringSet.of_list list in
       let tac_list, tac_prods = plist "simple_tactic" in
       let cmd_list, cmd_prods = plist "command" in
-      let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in
+      let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=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
@@ -1894,38 +1934,42 @@ let process_grammar args =
       if args.check_cmds then
         report_omitted_prods cmd_list !seen.cmds "Command" "\n                  ";
 *)
+      (* generate report on cmds or tacs *)
+      let cmdReport outfile cmdStr cmd_nts cmds cmdvs =
+        let rstCmds = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings cmds)) in
+        let rstCmdvs = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings cmdvs)) in
+        let gramCmds = List.fold_left (fun set nt ->
+            StringSet.union set (StringSet.of_list (List.map (fun p -> String.trim (prod_to_prodn p)) (NTMap.find nt !prodn_gram.map)))
+          ) StringSet.empty cmd_nts in
+        let allCmds = StringSet.union rstCmdvs (StringSet.union rstCmds gramCmds) in
+        let out = open_out_bin (dir outfile) in
+        StringSet.iter (fun c ->
+            let rsts = StringSet.mem c rstCmds in
+            let gram = StringSet.mem c gramCmds in
+            let pfx = match rsts, gram with
+            | true, false -> "+"
+            | false, true -> "-"
+            | false, false -> "?"
+            | _, _ -> " "
+            in
+            let var = if StringSet.mem c rstCmdvs then "v" else " " in
+            fprintf out "%s%s  %s\n" pfx var c)
+          allCmds;
+        close_out out;
+        Printf.printf "# %s in rsts, gram, total = %d %d %d\n" cmdStr (StringSet.cardinal gramCmds)
+          (StringSet.cardinal rstCmds) (StringSet.cardinal allCmds);
+      in
 
-      let rstCmds = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings !seen.cmds)) in
-      let rstCmdvs = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings !seen.cmdvs)) in
-      let command_nts = ["command"; "gallina"; "gallina_ext"; "query_command"; "syntax"] in
+      let cmd_nts = ["command"] in
       (* TODO: need to handle tactic_mode (overlaps with query_command) and subprf *)
-      let gramCmds = List.fold_left (fun set nt ->
-          StringSet.union set (StringSet.of_list (List.map (fun p -> String.trim (prod_to_prodn p)) (NTMap.find nt !prodn_gram.map)))
-        ) StringSet.empty command_nts in
-
-      let allCmds = StringSet.union rstCmdvs (StringSet.union rstCmds gramCmds) in
-      let out = open_out_bin (dir "prodnCommands") in
-      StringSet.iter (fun c ->
-          let rsts = StringSet.mem c rstCmds in
-          let gram = StringSet.mem c gramCmds in
-          let pfx = match rsts, gram with
-          | true, false -> "+"
-          | false, true -> "-"
-          | false, false -> "?"
-          | _, _ -> " "
-          in
-          let var = if StringSet.mem c rstCmdvs then "v" else " " in
-          fprintf out "%s%s  %s\n" pfx var c)
-        allCmds;
-      close_out out;
-      Printf.printf "# cmds in rsts, gram, total = %d %d %d\n" (StringSet.cardinal gramCmds)
-        (StringSet.cardinal rstCmds) (StringSet.cardinal allCmds);
+      cmdReport "prodnCommands" "cmds" cmd_nts !seen.cmds !seen.cmdvs;
+
+      let tac_nts = ["simple_tactic"] in
+      cmdReport "prodnTactics" "tacs" tac_nts !seen.tacs !seen.tacvs
     end;
 
-    (* generate output for prodn: simple_tactic, command, also for Ltac?? *)
+    (* generate prodnGrammar for reference *)
     if !exit_code = 0 && not args.verify then begin
-      let prodn_edits = read_mlg_edit "prodn.edit_mlg" in
-      apply_edit_file prodn_gram prodn_edits;
       let out = open_temp_bin (dir "prodnGrammar") in
       print_in_order out prodn_gram `PRODN !prodn_gram.order StringSet.empty;
       close_out out;
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 2d933e8f8a..38e7b781df 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1,19 +1,9 @@
-(* Defines the order to apply to editedGrammar to get productionlistGrammar.
+(* Defines the order to apply to editedGrammar to get the final grammar for the doc.
 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
 
-vernac_toplevel: [
-| "Drop" "."
-| "Quit" "."
-| "BackTo" num "."
-| "Show" "Goal" num "at" num "."
-| "Show" "Proof" "Diffs" OPT "removed" "."
-| vernac_control
-]
-
 tactic_mode: [
-| OPT toplevel_selector query_command
 | OPT toplevel_selector "{"
 | OPT toplevel_selector OPT ( "Info" num ) ltac_expr ltac_use_default
 | "par" ":" OPT ( "Info" num ) ltac_expr ltac_use_default
@@ -24,14 +14,6 @@ ltac_use_default: [
 | "..."
 ]
 
-vernac_control: [
-| "Time" vernac_control
-| "Redirect" string vernac_control
-| "Timeout" num vernac_control
-| "Fail" vernac_control
-| LIST0 ( "#[" LIST0 attr SEP "," "]" ) vernac
-]
-
 term: [
 | "forall" open_binders "," term
 | "fun" open_binders "=>" term
@@ -163,10 +145,26 @@ subsequent_letter: [
 | [ first_letter | digit | "'" | unicode_id_part ]
 ]
 
+firstorder_rhs: [
+| OPT firstorder_using
+| "with" LIST1 ident
+| OPT firstorder_using "with" LIST1 ident
+]
+
+where: [
+| "at" "top"
+| "at" "bottom"
+| "after" ident
+| "before" ident
+]
+
 vernacular: [
 | LIST0 ( OPT all_attrs [ command | ltac_expr ] "." )
 ]
 
+tacticals: [
+]
+
 all_attrs: [
 | LIST0 ( "#[" LIST0 attr SEP "," "]" ) LIST0 legacy_attr
 ]
@@ -345,18 +343,10 @@ pattern0: [
 | string
 ]
 
-vernac: [
-| LIST0 legacy_attr vernac_aux
-]
-
 vernac_aux: [
-| gallina "."
-| gallina_ext "."
 | command "."
 | tactic_mode "."
-| syntax "."
 | subprf
-| query_command
 ]
 
 subprf: [
@@ -365,30 +355,6 @@ subprf: [
 | "}"
 ]
 
-gallina: [
-| thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
-| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
-| [ "Definition" | "Example" ] ident_decl def_body
-| "Let" ident def_body
-| "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
-| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
-| "Variant" variant_definition LIST0 ( "with" variant_definition )
-| [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition )
-| "Class" inductive_definition LIST0 ( "with" inductive_definition )
-| "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
-| "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
-| "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
-| "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
-| "Scheme" scheme LIST0 ( "with" scheme )
-| "Combined" "Scheme" ident "from" LIST1 ident SEP ","
-| "Register" qualid "as" qualid
-| "Register" "Inline" qualid
-| "Primitive" ident OPT [ ":" term ] ":=" register_token
-| "Universe" LIST1 ident
-| "Universes" LIST1 ident
-| "Constraint" LIST1 univ_constraint SEP ","
-]
-
 fix_definition: [
 | ident_decl LIST0 binder OPT fixannot OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
 ]
@@ -402,12 +368,8 @@ decl_notation: [
 ]
 
 register_token: [
-| register_prim_token
 | "#int63_type"
 | "#float64_type"
-]
-
-register_prim_token: [
 | "#int63_head0"
 | "#int63_tail0"
 | "#int63_add"
@@ -512,13 +474,8 @@ ref_or_pattern_occ: [
 ]
 
 occs_nums: [
-| LIST1 num_or_var
-| "-" num_or_var LIST0 int_or_var
-]
-
-num_or_var: [
-| num
-| ident
+| LIST1 [ num | ident ]
+| "-" [ num | ident ] LIST0 int_or_var
 ]
 
 int_or_var: [
@@ -578,11 +535,6 @@ cofix_definition: [
 | ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
 ]
 
-scheme: [
-| scheme_kind
-| ident ":=" scheme_kind
-]
-
 scheme_kind: [
 | "Induction" "for" smart_qualid "Sort" sort_family
 | "Minimality" "for" smart_qualid "Sort" sort_family
@@ -598,50 +550,8 @@ sort_family: [
 | "Type"
 ]
 
-gallina_ext: [
-| "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder OPT of_module_type OPT ( ":=" LIST1 module_expr_inl SEP "<+" )
-| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" )
-| "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl
-| "Section" ident
-| "Chapter" ident
-| "End" ident
-| "Collection" ident ":=" section_subset_expr
-| "Require" OPT [ "Import" | "Export" ] LIST1 qualid
-| "From" qualid "Require" OPT [ "Import" | "Export" ] LIST1 qualid
-| "Import" LIST1 qualid
-| "Export" LIST1 qualid
-| "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
-| "Include" "Type" LIST1 module_type_inl SEP "<+"
-| "Transparent" LIST1 smart_qualid
-| "Opaque" LIST1 smart_qualid
-| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ]
-| "Canonical" OPT "Structure" ident_decl def_body
-| "Canonical" OPT "Structure" smart_qualid
-| "Coercion" qualid OPT univ_decl def_body
-| "Identity" "Coercion" ident ":" class ">->" class
-| "Coercion" qualid ":" class ">->" class
-| "Coercion" by_notation ":" class ">->" class
-| "Context" LIST1 binder
-| "Instance" instance_name ":" term hint_info [ ":=" "{" [ LIST1 field_def SEP ";" | ] "}" | ":=" term | ]
-| "Existing" "Instance" qualid hint_info
-| "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
-| "Existing" "Class" qualid
-| "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
-| "Implicit" [ "Type" | "Types" ] reserv_list
-| "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
-| "Export" "Set" LIST1 ident option_setting
-| "Export" "Unset" LIST1 ident
-]
-
-option_setting: [
-|
-| int
-| string
-]
-
 hint_info: [
 | "|" OPT num OPT one_term
-|
 ]
 
 module_binder: [
@@ -734,11 +644,6 @@ strategy_level: [
 | "transparent"
 ]
 
-instance_name: [
-| ident_decl LIST0 binder
-|
-]
-
 reserv_list: [
 | LIST1 ( "(" simple_reserv ")" )
 | simple_reserv
@@ -752,9 +657,8 @@ command: [
 | "Goal" term
 | "Declare" "Scope" ident
 | "Pwd"
-| "Cd"
-| "Cd" string
-| "Load" [ "Verbose" | ] [ string | ident ]
+| "Cd" OPT string
+| "Load" OPT "Verbose" [ string | ident ]
 | "Declare" "ML" "Module" LIST1 string
 | "Locate" locatable
 | "Add" "LoadPath" string "as" dirpath
@@ -804,101 +708,61 @@ command: [
 | "Print" "Namespace" dirpath
 | "Inspect" num
 | "Add" "ML" "Path" string
-| "Set" LIST1 ident option_setting
-| "Unset" LIST1 ident
+| OPT "Export" "Set" LIST1 ident OPT [ int | string ]
+| OPT "Export" "Unset" LIST1 ident
 | "Print" "Table" LIST1 ident
-| "Add" ident ident LIST1 option_ref_value
-| "Add" ident LIST1 option_ref_value
-| "Test" LIST1 ident "for" LIST1 option_ref_value
-| "Test" LIST1 ident
-| "Remove" ident ident LIST1 option_ref_value
-| "Remove" ident LIST1 option_ref_value
-| "Write" "State" ident
-| "Write" "State" string
-| "Restore" "State" ident
-| "Restore" "State" string
+| "Add" ident OPT ident LIST1 [ qualid | string ]
+| "Test" LIST1 ident OPT ( "for" LIST1 [ qualid | string ] )
+| "Remove" OPT ident ident LIST1 [ qualid | string ]
+| "Write" "State" [ ident | string ]
+| "Restore" "State" [ ident | string ]
 | "Reset" "Initial"
 | "Reset" ident
-| "Back"
-| "Back" num
-| "Debug" "On"
-| "Debug" "Off"
+| "Back" OPT num
+| "Debug" [ "On" | "Off" ]
 | "Declare" "Reduction" ident ":=" red_expr
 | "Declare" "Custom" "Entry" ident
 | "Derive" ident "SuchThat" one_term "As" ident      (* derive plugin *)
 | "Proof"
 | "Proof" "Mode" string
 | "Proof" term
-| "Abort"
-| "Abort" "All"
-| "Abort" ident
-| "Existential" num constr_body
+| "Abort" OPT [ "All" | ident ]
+| "Existential" num OPT ( ":" term ) ":=" term
 | "Admitted"
 | "Qed"
 | "Save" ident
-| "Defined"
-| "Defined" ident
+| "Defined" OPT ident
 | "Restart"
-| "Undo"
-| "Undo" num
-| "Undo" "To" num
-| "Focus"
-| "Focus" num
+| "Undo" OPT ( OPT "To" num )
+| "Focus" OPT num
 | "Unfocus"
 | "Unfocused"
-| "Show"
-| "Show" num
-| "Show" ident
+| "Show" OPT [ ident | num ]
 | "Show" "Existentials"
 | "Show" "Universes"
 | "Show" "Conjectures"
-| "Show" "Proof"
+| "Show" "Proof" OPT ( "Diffs" OPT "removed" )
 | "Show" "Intro"
 | "Show" "Intros"
 | "Show" "Match" qualid
 | "Guarded"
-| "Create" "HintDb" ident [ "discriminated" | ]
-| "Remove" "Hints" LIST1 qualid opt_hintbases
-| "Hint" hint opt_hintbases
+| "Create" "HintDb" ident OPT "discriminated"
+| "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
+| "Hint" hint OPT ( ":" LIST1 ident )
 | "Comments" LIST0 comment
-| "Declare" "Instance" ident_decl LIST0 binder ":" term hint_info
-| "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" 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" ltac_expr
-| "Solve" "All" "Obligations"
-| "Admit" "Obligations" "of" ident
-| "Admit" "Obligations"
+| "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
+| "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
+| "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr )
+| "Solve" "Obligation" int OPT ( "of" ident ) "with" ltac_expr
+| "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr )
+| "Solve" "All" "Obligations" OPT ( "with" ltac_expr )
+| "Admit" "Obligations" OPT ( "of" ident )
 | "Obligation" "Tactic" ":=" ltac_expr
 | "Show" "Obligation" "Tactic"
-| "Obligations" "of" ident
-| "Obligations"
-| "Preterm" "of" ident
-| "Preterm"
-| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident
-| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "as" ident
-| "Add" "Relation" one_term one_term "as" ident
-| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "as" ident
-| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
-| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
-| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
-| "Add" "Relation" one_term one_term "transitivity" "proved" "by" one_term "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "transitivity" "proved" "by" one_term "as" ident
+| "Obligations" OPT ( "of" ident )
+| "Preterm" OPT ( "of" ident )
+| "Add" "Relation" one_term one_term OPT ( "reflexivity" "proved" "by" one_term ) OPT ( "symmetry" "proved" "by" one_term ) OPT ( "transitivity" "proved" "by" one_term ) "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term OPT ( "reflexivity" "proved" "by" one_term ) OPT ( "symmetry" "proved" "by" one_term ) OPT ( "transitivity" "proved" "by" one_term ) "as" ident
 | "Add" "Setoid" one_term one_term one_term "as" ident
 | "Add" "Parametric" "Setoid" LIST0 binder ":" one_term one_term one_term "as" ident
 | "Add" "Morphism" one_term ":" ident
@@ -912,9 +776,7 @@ command: [
 | "Optimize" "Proof"
 | "Optimize" "Heap"
 | "Reset" "Ltac" "Profile"
-| "Show" "Ltac" "Profile"
-| "Show" "Ltac" "Profile" "CutOff" int
-| "Show" "Ltac" "Profile" string
+| "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ]
 | "Show" "Lia" "Profile"      (* micromega plugin *)
 | "Add" "InjTyp" one_term      (* micromega plugin *)
 | "Add" "BinOp" one_term      (* micromega plugin *)
@@ -935,10 +797,10 @@ command: [
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
 | "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* setoid_ring plugin *)
-| "Hint" "Cut" "[" hints_path "]" opthints
+| "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
-| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int
+| "Typeclasses" "eauto" ":=" OPT "debug" OPT [ "(bfs)" | "(dfs)" ] OPT int
 | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
 | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
 | "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr
@@ -967,20 +829,15 @@ command: [
 | "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
 | "Print" "Extraction" "Blacklist"      (* extraction plugin *)
 | "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
-| "Extract" "Constant" qualid LIST0 string "=>" mlname      (* extraction plugin *)
-| "Extract" "Inlined" "Constant" qualid "=>" mlname      (* extraction plugin *)
-| "Extract" "Inductive" qualid "=>" mlname "[" LIST0 mlname "]" OPT string      (* extraction plugin *)
+| "Extract" "Constant" qualid LIST0 string "=>" [ ident | string ]      (* extraction plugin *)
+| "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ]      (* extraction plugin *)
+| "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string      (* extraction plugin *)
 | "Show" "Extraction"      (* extraction plugin *)
 | "Functional" "Case" fun_scheme_arg      (* funind plugin *)
 | "Generate" "graph" "for" qualid      (* funind plugin *)
-| "Hint" "Rewrite" orient LIST1 one_term ":" LIST0 ident
-| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr ":" LIST0 ident
-| "Hint" "Rewrite" orient LIST1 one_term
-| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr
-| "Derive" "Inversion_clear" ident "with" one_term "Sort" sort_family
-| "Derive" "Inversion_clear" ident "with" one_term
-| "Derive" "Inversion" ident "with" one_term "Sort" sort_family
-| "Derive" "Inversion" ident "with" one_term
+| "Hint" "Rewrite" OPT [ "->" | "<-" ] LIST1 one_term OPT ( "using" ltac_expr ) OPT ( ":" LIST0 ident )
+| "Derive" "Inversion_clear" ident "with" one_term OPT ( "Sort" sort_family )
+| "Derive" "Inversion" ident "with" one_term OPT ( "Sort" sort_family )
 | "Derive" "Dependent" "Inversion" ident "with" one_term "Sort" sort_family
 | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family
 | "Declare" "Left" "Step" one_term
@@ -991,12 +848,86 @@ command: [
 | "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption
 | "String" "Notation" qualid qualid qualid ":" ident
 | "SubClass" ident_decl def_body
-]
-
-orient: [
-| "->"
-| "<-"
-|
+| thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
+| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
+| [ "Definition" | "Example" ] ident_decl def_body
+| "Let" ident def_body
+| "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
+| "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
+| "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
+| "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
+| "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
+| "Scheme" OPT ( ident ":=" ) scheme_kind LIST0 ( "with" OPT ( ident ":=" ) scheme_kind )
+| "Combined" "Scheme" ident "from" LIST1 ident SEP ","
+| "Register" qualid "as" qualid
+| "Register" "Inline" qualid
+| "Primitive" ident OPT [ ":" term ] ":=" register_token
+| "Universe" LIST1 ident
+| "Universes" LIST1 ident
+| "Constraint" LIST1 univ_constraint SEP ","
+| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
+| "Variant" variant_definition LIST0 ( "with" variant_definition )
+| [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition )
+| "Class" inductive_definition LIST0 ( "with" inductive_definition )
+| "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder OPT of_module_type OPT ( ":=" LIST1 module_expr_inl SEP "<+" )
+| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" )
+| "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl
+| "Section" ident
+| "Chapter" ident
+| "End" ident
+| "Collection" ident ":=" section_subset_expr
+| "Require" OPT [ "Import" | "Export" ] LIST1 qualid
+| "From" qualid "Require" OPT [ "Import" | "Export" ] LIST1 qualid
+| "Import" LIST1 qualid
+| "Export" LIST1 qualid
+| "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
+| "Include" "Type" LIST1 module_type_inl SEP "<+"
+| "Transparent" LIST1 smart_qualid
+| "Opaque" LIST1 smart_qualid
+| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ]
+| "Canonical" OPT "Structure" ident_decl def_body
+| "Canonical" OPT "Structure" smart_qualid
+| "Coercion" qualid OPT univ_decl def_body
+| "Identity" "Coercion" ident ":" class ">->" class
+| "Coercion" qualid ":" class ">->" class
+| "Coercion" by_notation ":" class ">->" class
+| "Context" LIST1 binder
+| "Instance" OPT ( ident_decl LIST0 binder ) ":" term OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ]
+| "Existing" "Instance" qualid OPT hint_info
+| "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
+| "Existing" "Class" qualid
+| "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| "Implicit" [ "Type" | "Types" ] reserv_list
+| "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
+| "Open" "Scope" ident
+| "Close" "Scope" ident
+| "Delimit" "Scope" ident "with" ident
+| "Undelimit" "Scope" ident
+| "Bind" "Scope" ident "with" LIST1 class
+| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
+| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
+| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
+| "Format" "Notation" string string string
+| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
+| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
+| "Eval" red_expr "in" term
+| "Compute" term
+| "Check" term
+| "About" smart_qualid OPT ( "@{" LIST0 name "}" )
+| "SearchHead" one_term OPT ne_in_or_out_modules
+| "SearchPattern" one_term OPT ne_in_or_out_modules
+| "SearchRewrite" one_term OPT ne_in_or_out_modules
+| "Search" searchabout_query OPT searchabout_queries
+| "SearchAbout" searchabout_query OPT searchabout_queries
+| "SearchAbout" "[" LIST1 searchabout_query "]" OPT ne_in_or_out_modules
+| "Time" command
+| "Redirect" string command
+| "Timeout" num command
+| "Fail" command
+| "Drop"
+| "Quit"
+| "BackTo" num
+| "Show" "Goal" num "at" num
 ]
 
 section_subset_expr: [
@@ -1047,27 +978,17 @@ locatable: [
 | "Module" qualid
 ]
 
-option_ref_value: [
-| qualid
-| string
-]
-
 comment: [
 | one_term
 | string
 | num
 ]
 
-reference_or_constr: [
-| qualid
-| one_term
-]
-
 hint: [
-| "Resolve" LIST1 reference_or_constr hint_info
+| "Resolve" LIST1 [ qualid | one_term ] OPT hint_info
 | "Resolve" "->" LIST1 qualid OPT num
 | "Resolve" "<-" LIST1 qualid OPT num
-| "Immediate" LIST1 reference_or_constr
+| "Immediate" LIST1 [ qualid | one_term ]
 | "Variables" "Transparent"
 | "Variables" "Opaque"
 | "Constants" "Transparent"
@@ -1080,24 +1001,9 @@ hint: [
 | "Extern" num OPT one_term "=>" ltac_expr
 ]
 
-constr_body: [
-| ":=" term
-| ":" term ":=" term
-]
-
-withtac: [
-| "with" ltac_expr
-|
-]
-
-ltac_def_kind: [
-| ":="
-| "::="
-]
-
 tacdef_body: [
-| qualid LIST1 fun_var ltac_def_kind ltac_expr
-| qualid ltac_def_kind ltac_expr
+| qualid LIST1 fun_var [ ":=" | "::=" ] ltac_expr
+| qualid [ ":=" | "::=" ] ltac_expr
 ]
 
 ltac_production_item: [
@@ -1111,11 +1017,6 @@ numnotoption: [
 | "(" "abstract" "after" bignat ")"
 ]
 
-mlname: [
-| ident      (* extraction plugin *)
-| string      (* extraction plugin *)
-]
-
 int_or_id: [
 | ident      (* extraction plugin *)
 | int      (* extraction plugin *)
@@ -1153,55 +1054,17 @@ field_mod: [
 | "completeness" one_term      (* setoid_ring plugin *)
 ]
 
-debug: [
-| "debug"
-|
-]
-
-eauto_search_strategy: [
-| "(bfs)"
-| "(dfs)"
-|
-]
-
-hints_path_atom: [
-| LIST1 qualid
-| "_"
-]
-
 hints_path: [
 | "(" hints_path ")"
 | hints_path "*"
 | "emp"
 | "eps"
 | hints_path "|" hints_path
-| hints_path_atom
+| LIST1 qualid
+| "_"
 | hints_path hints_path
 ]
 
-opthints: [
-| ":" LIST1 ident
-|
-]
-
-opt_hintbases: [
-|
-| ":" LIST1 ident
-]
-
-query_command: [
-| "Eval" red_expr "in" term "."
-| "Compute" term "."
-| "Check" term "."
-| "About" smart_qualid OPT ( "@{" LIST0 name "}" ) "."
-| "SearchHead" one_term in_or_out_modules "."
-| "SearchPattern" one_term in_or_out_modules "."
-| "SearchRewrite" one_term in_or_out_modules "."
-| "Search" searchabout_query searchabout_queries "."
-| "SearchAbout" searchabout_query searchabout_queries "."
-| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
-]
-
 class: [
 | "Funclass"
 | "Sortclass"
@@ -1213,39 +1076,14 @@ ne_in_or_out_modules: [
 | "outside" LIST1 qualid
 ]
 
-in_or_out_modules: [
-| ne_in_or_out_modules
-|
-]
-
-positive_search_mark: [
-| "-"
-|
-]
-
 searchabout_query: [
-| positive_search_mark string OPT ( "%" ident )
-| positive_search_mark one_term
+| OPT "-" string OPT ( "%" ident )
+| OPT "-" one_term
 ]
 
 searchabout_queries: [
 | ne_in_or_out_modules
 | searchabout_query searchabout_queries
-|
-]
-
-syntax: [
-| "Open" "Scope" ident
-| "Close" "Scope" ident
-| "Delimit" "Scope" ident "with" ident
-| "Undelimit" "Scope" ident
-| "Bind" "Scope" ident "with" LIST1 class
-| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
-| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
-| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
-| "Format" "Notation" string string string
-| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
-| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
 ]
 
 level: [
@@ -1281,18 +1119,13 @@ syntax_extension_type: [
 | "bigint"
 | "binder"
 | "constr"
-| "constr" at_level_opt OPT constr_as_binder_kind
+| "constr" OPT ( "at" level ) OPT constr_as_binder_kind
 | "pattern"
 | "pattern" "at" "level" num
 | "strict" "pattern"
 | "strict" "pattern" "at" "level" num
 | "closed" "binder"
-| "custom" ident at_level_opt OPT constr_as_binder_kind
-]
-
-at_level_opt: [
-| "at" level
-|
+| "custom" ident OPT ( "at" level ) OPT constr_as_binder_kind
 ]
 
 simple_tactic: [
@@ -1308,125 +1141,71 @@ simple_tactic: [
 | "elimtype" one_term
 | "lapply" one_term
 | "transitivity" one_term
-| "left"
-| "eleft"
-| "left" "with" bindings
-| "eleft" "with" bindings
-| "right"
-| "eright"
-| "right" "with" bindings
-| "eright" "with" bindings
-| "constructor"
-| "constructor" int_or_var
-| "constructor" int_or_var "with" bindings
-| "econstructor"
-| "econstructor" int_or_var
-| "econstructor" int_or_var "with" bindings
-| "specialize" constr_with_bindings
-| "specialize" constr_with_bindings "as" simple_intropattern
-| "symmetry"
-| "symmetry" "in" in_clause
-| "split"
-| "esplit"
-| "split" "with" bindings
-| "esplit" "with" bindings
-| "exists"
-| "exists" LIST1 bindings SEP ","
-| "eexists"
-| "eexists" LIST1 bindings SEP ","
-| "intros" "until" quantified_hypothesis
-| "intro"
-| "intro" ident
-| "intro" ident "at" "top"
-| "intro" ident "at" "bottom"
-| "intro" ident "after" ident
-| "intro" ident "before" ident
-| "intro" "at" "top"
-| "intro" "at" "bottom"
-| "intro" "after" ident
-| "intro" "before" ident
-| "move" ident "at" "top"
-| "move" ident "at" "bottom"
-| "move" ident "after" ident
-| "move" ident "before" ident
-| "rename" LIST1 rename SEP ","
+| "left" OPT ( "with" bindings )
+| "eleft" OPT ( "with" bindings )
+| "right" OPT ( "with" bindings )
+| "eright" OPT ( "with" bindings )
+| "constructor" OPT int_or_var OPT ( "with" bindings )
+| "econstructor" OPT ( int_or_var OPT ( "with" bindings ) )
+| "specialize" constr_with_bindings OPT ( "as" simple_intropattern )
+| "symmetry" OPT ( "in" in_clause )
+| "split" OPT ( "with" bindings )
+| "esplit" OPT ( "with" bindings )
+| "exists" OPT ( LIST1 bindings SEP "," )
+| "eexists" OPT ( LIST1 bindings SEP "," )
+| "intros" "until" [ ident | num ]
+| "intro" OPT ident OPT where
+| "move" ident OPT where
+| "rename" LIST1 ( ident "into" ident ) SEP ","
 | "revert" LIST1 ident
-| "simple" "induction" quantified_hypothesis
-| "simple" "destruct" quantified_hypothesis
-| "double" "induction" quantified_hypothesis quantified_hypothesis
+| "simple" "induction" [ ident | num ]
+| "simple" "destruct" [ ident | num ]
+| "double" "induction" [ ident | num ] [ ident | num ]
 | "admit"
-| "fix" ident num
-| "cofix" ident
 | "clear" LIST0 ident
 | "clear" "-" LIST1 ident
 | "clearbody" LIST1 ident
 | "generalize" "dependent" one_term
-| "replace" one_term "with" one_term clause_dft_concl by_arg_tac
-| "replace" "->" one_term clause_dft_concl
-| "replace" "<-" one_term clause_dft_concl
-| "replace" one_term clause_dft_concl
-| "simplify_eq"
-| "simplify_eq" destruction_arg
-| "esimplify_eq"
-| "esimplify_eq" destruction_arg
-| "discriminate"
-| "discriminate" destruction_arg
-| "ediscriminate"
-| "ediscriminate" destruction_arg
-| "injection"
-| "injection" destruction_arg
-| "einjection"
-| "einjection" destruction_arg
-| "injection" "as" LIST0 simple_intropattern
-| "injection" destruction_arg "as" LIST0 simple_intropattern
-| "einjection" "as" LIST0 simple_intropattern
-| "einjection" destruction_arg "as" LIST0 simple_intropattern
-| "simple" "injection"
-| "simple" "injection" destruction_arg
-| "dependent" "rewrite" orient one_term
-| "dependent" "rewrite" orient one_term "in" ident
-| "cutrewrite" orient one_term
-| "cutrewrite" orient one_term "in" ident
+| "replace" one_term "with" one_term OPT clause_dft_concl OPT ( "by" ltac_expr3 )
+| "replace" OPT [ "->" | "<-" ] one_term OPT clause_dft_concl
+| "simplify_eq" OPT destruction_arg
+| "esimplify_eq" OPT destruction_arg
+| "discriminate" OPT destruction_arg
+| "ediscriminate" OPT destruction_arg
+| "injection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern )
+| "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern )
+| "simple" "injection" OPT destruction_arg
+| "dependent" "rewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
+| "cutrewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
 | "decompose" "sum" one_term
 | "decompose" "record" one_term
 | "absurd" one_term
 | "contradiction" OPT constr_with_bindings
-| "autorewrite" "with" LIST1 ident clause_dft_concl
-| "autorewrite" "with" LIST1 ident clause_dft_concl "using" ltac_expr
-| "autorewrite" "*" "with" LIST1 ident clause_dft_concl
-| "autorewrite" "*" "with" LIST1 ident clause_dft_concl "using" ltac_expr
-| "rewrite" "*" orient one_term "in" ident "at" occurrences by_arg_tac
-| "rewrite" "*" orient one_term "at" occurrences "in" ident by_arg_tac
-| "rewrite" "*" orient one_term "in" ident by_arg_tac
-| "rewrite" "*" orient one_term "at" occurrences by_arg_tac
-| "rewrite" "*" orient one_term by_arg_tac
+| "autorewrite" OPT "*" "with" LIST1 ident OPT clause_dft_concl OPT ( "using" ltac_expr )
+| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" occurrences OPT ( "by" ltac_expr3 ) )
+| "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" occurrences "in" ident OPT ( "by" ltac_expr3 )
 | "refine" one_term
 | "simple" "refine" one_term
 | "notypeclasses" "refine" one_term
 | "simple" "notypeclasses" "refine" one_term
 | "solve_constraints"
-| "subst" LIST1 ident
-| "subst"
+| "subst" OPT ( LIST1 ident )
 | "simple" "subst"
 | "evar" "(" ident ":" term ")"
 | "evar" one_term
 | "instantiate" "(" ident ":=" term ")"
-| "instantiate" "(" int ":=" term ")" hloc
+| "instantiate" "(" int ":=" term ")" OPT hloc
 | "instantiate"
-| "stepl" one_term "by" ltac_expr
-| "stepl" one_term
-| "stepr" one_term "by" ltac_expr
-| "stepr" one_term
+| "stepl" one_term OPT ( "by" ltac_expr )
+| "stepr" one_term OPT ( "by" ltac_expr )
 | "generalize_eqs" ident
 | "dependent" "generalize_eqs" ident
 | "generalize_eqs_vars" ident
 | "dependent" "generalize_eqs_vars" ident
 | "specialize_eqs" ident
-| "hresolve_core" "(" ident ":=" one_term ")" "at" int_or_var "in" one_term
-| "hresolve_core" "(" ident ":=" one_term ")" "in" one_term
+| "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" int_or_var ) "in" one_term
 | "hget_evar" int_or_var
-| "destauto"
-| "destauto" "in" ident
+| "destauto" OPT ( "in" ident )
 | "transparent_abstract" ltac_expr3
 | "transparent_abstract" ltac_expr3 "using" ident
 | "constr_eq" one_term one_term
@@ -1458,27 +1237,24 @@ simple_tactic: [
 | "show" "ltac" "profile" "cutoff" int
 | "show" "ltac" "profile" string
 | "restart_timer" OPT string
-| "finish_timing" OPT string
-| "finish_timing" "(" string ")" OPT string
+| "finish_timing" OPT ( "(" string ")" ) OPT string
 | "eassumption"
 | "eexact" one_term
-| "trivial" auto_using hintbases
-| "info_trivial" auto_using hintbases
-| "debug" "trivial" auto_using hintbases
-| "auto" OPT int_or_var auto_using hintbases
-| "info_auto" OPT int_or_var auto_using hintbases
-| "debug" "auto" OPT int_or_var auto_using hintbases
+| "trivial" OPT auto_using OPT hintbases
+| "info_trivial" OPT auto_using OPT hintbases
+| "debug" "trivial" OPT auto_using OPT hintbases
+| "auto" OPT int_or_var OPT auto_using OPT hintbases
+| "info_auto" OPT int_or_var OPT auto_using OPT hintbases
+| "debug" "auto" OPT int_or_var OPT auto_using OPT hintbases
 | "prolog" "[" LIST0 one_term "]" int_or_var
-| "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
-| "new" "auto" OPT int_or_var auto_using hintbases
-| "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
-| "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases
-| "dfs" "eauto" OPT int_or_var auto_using hintbases
-| "autounfold" hintbases clause_dft_concl
-| "autounfold_one" hintbases "in" ident
-| "autounfold_one" hintbases
-| "unify" one_term one_term
-| "unify" one_term one_term "with" ident
+| "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
+| "new" "auto" OPT int_or_var OPT auto_using OPT hintbases
+| "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
+| "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
+| "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases
+| "autounfold" OPT hintbases OPT clause_dft_concl
+| "autounfold_one" OPT hintbases OPT ( "in" ident )
+| "unify" one_term one_term OPT ( "with" ident )
 | "convert_concl_no_check" one_term
 | "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 ident
 | "typeclasses" "eauto" OPT int_or_var "with" LIST1 ident
@@ -1489,103 +1265,90 @@ simple_tactic: [
 | "autoapply" one_term "using" ident
 | "autoapply" one_term "with" ident
 | "progress_evars" ltac_expr
-| "rewrite_strat" rewstrategy
-| "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" ident
+| "rewrite_strat" rewstrategy OPT ( "in" ident )
+| "rewrite_db" ident OPT ( "in" ident )
+| "substitute" OPT [ "->" | "<-" ] constr_with_bindings
+| "setoid_rewrite" OPT [ "->" | "<-" ] constr_with_bindings OPT ( "at" occurrences ) OPT ( "in" ident )
+| "setoid_rewrite" OPT [ "->" | "<-" ] constr_with_bindings "in" ident "at" occurrences
+| "setoid_symmetry" OPT ( "in" ident )
 | "setoid_reflexivity"
 | "setoid_transitivity" one_term
 | "setoid_etransitivity"
 | "decide" "equality"
 | "compare" one_term one_term
-| "rewrite_strat" rewstrategy "in" ident
-| "intros" intropattern_list_opt
-| "eintros" intropattern_list_opt
-| "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
-| "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
-| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
-| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
+| "intros" LIST0 intropattern
+| "eintros" LIST0 intropattern
+| "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
+| "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
+| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
+| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
 | "elim" constr_with_bindings_arg OPT ( "using" constr_with_bindings )
 | "eelim" constr_with_bindings_arg OPT ( "using" constr_with_bindings )
 | "case" induction_clause_list
 | "ecase" induction_clause_list
-| "fix" ident num "with" LIST1 fixdecl
-| "cofix" ident "with" LIST1 cofixdecl
+| "fix" ident num OPT ( "with" LIST1 fixdecl )
+| "cofix" ident OPT ( "with" LIST1 cofixdecl )
 | "pose" bindings_with_parameters
-| "pose" one_term as_name
+| "pose" one_term OPT as_name
 | "epose" bindings_with_parameters
-| "epose" one_term as_name
-| "set" bindings_with_parameters clause_dft_concl
-| "set" one_term as_name clause_dft_concl
-| "eset" bindings_with_parameters clause_dft_concl
-| "eset" one_term as_name clause_dft_concl
-| "remember" one_term as_name eqn_ipat clause_dft_all
-| "eremember" one_term as_name eqn_ipat clause_dft_all
+| "epose" one_term OPT as_name
+| "set" bindings_with_parameters OPT clause_dft_concl
+| "set" one_term OPT as_name OPT clause_dft_concl
+| "eset" bindings_with_parameters OPT clause_dft_concl
+| "eset" one_term OPT as_name OPT clause_dft_concl
+| "remember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all
+| "eremember" one_term OPT as_name OPT eqn_ipat OPT 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" one_term as_ipat by_tactic
-| "eassert" one_term as_ipat by_tactic
+| "assert" "(" ident ":" term ")" OPT ( "by" ltac_expr3 )
+| "eassert" "(" ident ":" term ")" OPT ( "by" ltac_expr3 )
+| "enough" "(" ident ":" term ")" OPT ( "by" ltac_expr3 )
+| "eenough" "(" ident ":" term ")" OPT ( "by" ltac_expr3 )
+| "assert" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
+| "eassert" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
 | "pose" "proof" "(" ident ":=" term ")"
 | "epose" "proof" "(" ident ":=" term ")"
-| "pose" "proof" term as_ipat
-| "epose" "proof" term as_ipat
-| "enough" one_term as_ipat by_tactic
-| "eenough" one_term as_ipat by_tactic
-| "generalize" one_term
-| "generalize" one_term LIST1 one_term
-| "generalize" one_term OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ]
+| "pose" "proof" term OPT as_ipat
+| "epose" "proof" term OPT as_ipat
+| "enough" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
+| "eenough" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
+| "generalize" one_term OPT ( LIST1 one_term )
+| "generalize" one_term OPT ( "at" occs_nums ) OPT as_name LIST0 [ "," pattern_occ OPT as_name ]
 | "induction" induction_clause_list
 | "einduction" induction_clause_list
 | "destruct" induction_clause_list
 | "edestruct" induction_clause_list
-| "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
-| "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
-| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" one_term ]
-| "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" one_term in_hyp_list
-| "red" clause_dft_concl
-| "hnf" clause_dft_concl
-| "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl
-| "cbv" OPT strategy_flag clause_dft_concl
-| "cbn" OPT strategy_flag clause_dft_concl
-| "lazy" OPT strategy_flag clause_dft_concl
-| "compute" OPT delta_flag clause_dft_concl
-| "vm_compute" OPT ref_or_pattern_occ clause_dft_concl
-| "native_compute" OPT ref_or_pattern_occ clause_dft_concl
-| "unfold" LIST1 unfold_occ SEP "," clause_dft_concl
-| "fold" LIST1 one_term clause_dft_concl
-| "pattern" LIST1 pattern_occ SEP "," clause_dft_concl
-| "change" conversion clause_dft_concl
-| "change_no_check" conversion clause_dft_concl
+| "rewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
+| "erewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
+| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | num ] OPT as_or_and_ipat OPT [ "with" one_term ]
+| "simple" "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
+| "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
+| "inversion_clear" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
+| "inversion" [ ident | num ] "using" one_term OPT ( "in" LIST1 ident )
+| "red" OPT clause_dft_concl
+| "hnf" OPT clause_dft_concl
+| "simpl" OPT delta_flag OPT ref_or_pattern_occ OPT clause_dft_concl
+| "cbv" OPT strategy_flag OPT clause_dft_concl
+| "cbn" OPT strategy_flag OPT clause_dft_concl
+| "lazy" OPT strategy_flag OPT clause_dft_concl
+| "compute" OPT delta_flag OPT clause_dft_concl
+| "vm_compute" OPT ref_or_pattern_occ OPT clause_dft_concl
+| "native_compute" OPT ref_or_pattern_occ OPT clause_dft_concl
+| "unfold" LIST1 unfold_occ SEP "," OPT clause_dft_concl
+| "fold" LIST1 one_term OPT clause_dft_concl
+| "pattern" LIST1 pattern_occ SEP "," OPT clause_dft_concl
+| "change" conversion OPT clause_dft_concl
+| "change_no_check" conversion OPT clause_dft_concl
 | "btauto"
 | "rtauto"
-| "congruence"
-| "congruence" int
-| "congruence" "with" LIST1 one_term
-| "congruence" int "with" LIST1 one_term
+| "congruence" OPT int OPT ( "with" LIST1 one_term )
 | "f_equal"
-| "firstorder" OPT ltac_expr firstorder_using
-| "firstorder" OPT ltac_expr "with" LIST1 ident
-| "firstorder" OPT ltac_expr firstorder_using "with" LIST1 ident
+| "firstorder" OPT ltac_expr firstorder_rhs
 | "gintuition" OPT ltac_expr
-| "functional" "inversion" quantified_hypothesis OPT qualid      (* funind plugin *)
-| "functional" "induction" LIST1 one_term fun_ind_using with_names      (* funind plugin *)
-| "soft" "functional" "induction" LIST1 one_term fun_ind_using with_names      (* funind plugin *)
-| "psatz_Z" int_or_var ltac_expr      (* micromega plugin *)
-| "psatz_Z" ltac_expr      (* micromega plugin *)
+| "functional" "inversion" [ ident | num ] OPT qualid      (* funind plugin *)
+| "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names      (* funind plugin *)
+| "soft" "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names      (* funind plugin *)
+| "psatz_Z" OPT int_or_var ltac_expr
 | "xlia" ltac_expr      (* micromega plugin *)
 | "xnlia" ltac_expr      (* micromega plugin *)
 | "xnra" ltac_expr      (* micromega plugin *)
@@ -1595,10 +1358,8 @@ simple_tactic: [
 | "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 *)
+| "psatz_R" OPT int_or_var ltac_expr
+| "psatz_Q" OPT int_or_var ltac_expr
 | "zify_iter_specs"      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
 | "zify_saturate"      (* micromega plugin *)
@@ -1606,14 +1367,37 @@ simple_tactic: [
 | "zify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" one_term      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
-| "protect_fv" string "in" ident      (* setoid_ring plugin *)
-| "protect_fv" string      (* setoid_ring plugin *)
+| "protect_fv" string OPT ( "in" ident )
 | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
 | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
+| "classical_left"
+| "classical_right"
+| "contradict" ident
+| "discrR"
+| "easy"
+| "exfalso"
+| "inversion_sigma"
+| "lia"
+| "lra"
+| "nia"
+| "nra"
+| "split_Rabs"
+| "split_Rmult"
+| "tauto"
+| "zify"
+| "assert_fails" ltac_expr3
+| "assert_succeeds" ltac_expr3
+| "field" OPT ( "[" LIST1 term "]" )
+| "field_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
+| "field_simplify_eq" OPT ( "[" LIST1 term "]" ) OPT ( "in" ident )
+| "intuition" OPT ltac_expr
+| "nsatz" OPT ( "with" "radicalmax" ":=" term "strategy" ":=" term "parameters" ":=" term "variables" ":=" term )
+| "psatz" term OPT int_or_var
+| "ring" OPT ( "[" LIST1 term "]" )
+| "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
 ]
 
 hloc: [
-|
 | "in" "|-" "*"
 | "in" ident
 | "in" "(" "Type" "of" ident ")"
@@ -1622,15 +1406,6 @@ hloc: [
 | "in" "(" "value" "of" ident ")"
 ]
 
-rename: [
-| ident "into" ident
-]
-
-by_arg_tac: [
-| "by" ltac_expr3
-|
-]
-
 in_clause: [
 | LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ )
 | "*" "|-" OPT concl_occ
@@ -1653,7 +1428,6 @@ hypident: [
 
 as_ipat: [
 | "as" simple_intropattern
-|
 ]
 
 or_and_intropattern_loc: [
@@ -1663,29 +1437,21 @@ or_and_intropattern_loc: [
 
 as_or_and_ipat: [
 | "as" or_and_intropattern_loc
-|
 ]
 
 eqn_ipat: [
 | "eqn" ":" naming_intropattern
 | "_eqn" ":" naming_intropattern
 | "_eqn"
-|
 ]
 
 as_name: [
 | "as" ident
-|
-]
-
-by_tactic: [
-| "by" ltac_expr3
-|
 ]
 
 rewriter: [
 | "!" constr_with_bindings_arg
-| [ "?" | "?" ] constr_with_bindings_arg
+| "?" constr_with_bindings_arg
 | num "!" constr_with_bindings_arg
 | num [ "?" | "?" ] constr_with_bindings_arg
 | num constr_with_bindings_arg
@@ -1693,24 +1459,19 @@ rewriter: [
 ]
 
 oriented_rewriter: [
-| orient rewriter
+| OPT [ "->" | "<-" ] rewriter
 ]
 
 induction_clause: [
-| destruction_arg as_or_and_ipat eqn_ipat opt_clause
+| destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause
 ]
 
 induction_clause_list: [
-| LIST1 induction_clause SEP "," OPT ( "using" constr_with_bindings ) opt_clause
+| LIST1 induction_clause SEP "," OPT ( "using" constr_with_bindings ) OPT opt_clause
 ]
 
 auto_using: [
 | "using" LIST1 one_term SEP ","
-|
-]
-
-intropattern_list_opt: [
-| LIST0 intropattern
 ]
 
 or_and_intropattern: [
@@ -1720,14 +1481,13 @@ or_and_intropattern: [
 ]
 
 intropattern_or_list_or: [
-| intropattern_or_list_or "|" intropattern_list_opt
-| intropattern_list_opt
+| LIST0 intropattern LIST0 ( "|" LIST0 intropattern )
 ]
 
 equality_intropattern: [
 | "->"
 | "<-"
-| "[=" intropattern_list_opt "]"
+| "[=" LIST0 intropattern "]"
 ]
 
 naming_intropattern: [
@@ -1774,7 +1534,6 @@ comparison: [
 hintbases: [
 | "with" "*"
 | "with" LIST1 ident
-|
 ]
 
 bindings_with_parameters: [
@@ -1784,28 +1543,19 @@ bindings_with_parameters: [
 clause_dft_concl: [
 | "in" in_clause
 | OPT ( "at" occs_nums )
-|
 ]
 
 clause_dft_all: [
 | "in" in_clause
-|
 ]
 
 opt_clause: [
 | "in" in_clause
 | "at" occs_nums
-|
-]
-
-in_hyp_list: [
-| "in" LIST1 ident
-|
 ]
 
 in_hyp_as: [
-| "in" ident as_ipat
-|
+| "in" ident OPT as_ipat
 ]
 
 simple_binder: [
@@ -1814,12 +1564,11 @@ simple_binder: [
 ]
 
 fixdecl: [
-| "(" ident LIST0 simple_binder struct_annot ":" term ")"
+| "(" ident LIST0 simple_binder OPT struct_annot ":" term ")"
 ]
 
 struct_annot: [
 | "{" "struct" name "}"
-|
 ]
 
 cofixdecl: [
@@ -1827,12 +1576,7 @@ cofixdecl: [
 ]
 
 constr_with_bindings: [
-| one_term with_bindings
-]
-
-with_bindings: [
-| "with" bindings
-|
+| one_term OPT ( "with" bindings )
 ]
 
 destruction_arg: [
@@ -1846,11 +1590,6 @@ constr_with_bindings_arg: [
 | constr_with_bindings
 ]
 
-quantified_hypothesis: [
-| ident
-| num
-]
-
 conversion: [
 | one_term
 | one_term "with" one_term
@@ -1861,17 +1600,14 @@ firstorder_using: [
 | "using" qualid
 | "using" qualid "," LIST1 qualid SEP ","
 | "using" qualid qualid LIST0 qualid
-|
 ]
 
 fun_ind_using: [
 | "using" constr_with_bindings      (* funind plugin *)
-|      (* funind plugin *)
 ]
 
 with_names: [
 | "as" simple_intropattern      (* funind plugin *)
-|      (* funind plugin *)
 ]
 
 occurrences: [
@@ -2019,16 +1755,11 @@ tactic_arg: [
 | "eval" red_expr "in" term
 | "context" ident "[" term "]"
 | "type" "of" term
-| "fresh" LIST0 fresh_id
+| "fresh" LIST0 [ string | qualid ]
 | "type_term" one_term
 | "numgoals"
 ]
 
-fresh_id: [
-| string
-| qualid
-]
-
 tactic_arg_compat: [
 | tactic_arg
 | term
diff --git a/doc/tools/docgram/prodn.edit_mlg b/doc/tools/docgram/prodn.edit_mlg
deleted file mode 100644
index 8bd8cad6b5..0000000000
--- a/doc/tools/docgram/prodn.edit_mlg
+++ /dev/null
@@ -1,24 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Defines additional productions and edits for use in documentation.  Not compiled into Coq *)
-(* 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
deleted file mode 100644
index 641ab8fbe5..0000000000
--- a/doc/tools/docgram/productionlist.edit_mlg
+++ /dev/null
@@ -1,14 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Defines additional productions and edits for use in documentation.  Not compiled into Coq *)
-(* Contents used to generate productionlists in doc *)
-
-DOC_GRAMMAR