Merge PR #13219: Rename mlg grammar nonterminals to make documented and mlg grammars more consistent

Reviewed-by: Zimmi48
Reviewed-by: herbelin
Ack-by: SkySkimmer

8 files changed, 532 insertions, 613 deletions

diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 122b0f5dfb..ba0ec28f8b 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -342,9 +342,9 @@ Recursive functions: fix
 .. insertprodn term_fix fixannot
 
 .. prodn::
-   term_fix ::= let fix @fix_body in @term
-   | fix @fix_body {? {+ with @fix_body } for @ident }
-   fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term
+   term_fix ::= let fix @fix_decl in @term
+   | fix @fix_decl {? {+ with @fix_decl } for @ident }
+   fix_decl ::= @ident {* @binder } {? @fixannot } {? : @type } := @term
    fixannot ::= %{ struct @ident %}
    | %{ wf @one_term @ident %}
    | %{ measure @one_term {? @ident } {? @one_term } %}
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 5c091f04ac..8663ac646b 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -161,7 +161,7 @@ Syntactic values
 Provides a way to use the syntax and semantics of a grammar nonterminal as a
 value in an :token:`ltac_expr`.  The table below describes the most useful of
 these.  You can see the others by running ":cmd:`Print Grammar` `tactic`" and
-examining the part at the end under "Entry tactic:tactic_arg".
+examining the part at the end under "Entry tactic:tactic_value".
 
    :token:`ident`
       name of a grammar nonterminal listed in the table
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 770de9a6c3..cdbae8ade1 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -5724,11 +5724,11 @@ respectively.
 
    local function definition
 
-.. tacv:: pose fix @fix_body
+.. tacv:: pose fix @fix_decl
 
    local fix definition
 
-.. tacv:: pose cofix @fix_body
+.. tacv:: pose cofix @fix_decl
 
    local cofix definition
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 0c51361b64..06018304ab 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -444,7 +444,7 @@ Displaying information about notations
 
    This command doesn't display all nonterminals of the grammar.  For example,
    productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality`
-   and `tactic_then_gen` which are not shown and can't be printed.
+   and `for_each_goal` which are not shown and can't be printed.
 
    Most of the grammar in the documentation was updated in 8.12 to make it accurate and
    readable.  This was done using a new developer tool that extracts the grammar from the
@@ -477,16 +477,16 @@ Displaying information about notations
    such as `1+2*3` in the usual way as `1+(2*3)`.  However, most nonterminals have a single level.
 
    For example, this output from `Print Grammar tactic` shows the first 3 levels for
-   `tactic_expr`, designated as "5", "4" and "3".  Level 3 is right-associative,
+   `ltac_expr`, designated as "5", "4" and "3".  Level 3 is right-associative,
    which applies to the productions within it, such as the `try` construct::
 
-     Entry tactic_expr is
+     Entry ltac_expr is
      [ "5" RIGHTA
        [ binder_tactic ]
      | "4" LEFTA
        [ SELF; ";"; binder_tactic
        | SELF; ";"; SELF
-       | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ]
+       | SELF; ";"; tactic_then_locality; for_each_goal; "]" ]
      | "3" RIGHTA
        [ IDENT "try"; SELF
        :
@@ -510,7 +510,7 @@ Displaying information about notations
 
    The output for `Print Grammar constr` includes :cmd:`Notation` definitions,
    which are dynamically added to the grammar at run time.
-   For example, in the definition for `operconstr`, the production on the second line shown
+   For example, in the definition for `term`, the production on the second line shown
    here is defined by a :cmd:`Reserved Notation` command in `Notations.v`::
 
      | "50" LEFTA
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 4d38955fa8..dbb04bb6a6 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -42,7 +42,7 @@ for documentation purposes:
     First, nonterminals that use levels (`"5" RIGHTA` below) are modified, for example:
 
     ```
-    tactic_expr:
+    ltac_expr:
       [ "5" RIGHTA
         [ te = binder_tactic -> { te } ]
       [ "4"   ...
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index f9aba5b1e1..f6a684bbd7 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -28,15 +28,15 @@ strategy_level_or_var: [
 | strategy_level
 ]
 
-operconstr0: [
-| "ltac" ":" "(" tactic_expr5 ")"
+term0: [
+| "ltac" ":" "(" ltac_expr5 ")"
 ]
 
 EXTRAARGS_natural: [ | DELETENT ]
 EXTRAARGS_lconstr:  [ | DELETENT ]
 EXTRAARGS_strategy_level: [ | DELETENT ]
 G_LTAC_hint: [ | DELETENT ]
-G_LTAC_operconstr0: [ | DELETENT ]
+G_LTAC_term0: [ | DELETENT ]
 
 G_REWRITE_binders: [
 | DELETE Pcoq.Constr.binders
@@ -86,7 +86,7 @@ RENAME: [
 | G_LTAC2_eqn_ipat ltac2_eqn_ipat
 | G_LTAC2_conversion ltac2_conversion
 | G_LTAC2_oriented_rewriter ltac2_oriented_rewriter
-| G_LTAC2_tactic_then_gen ltac2_tactic_then_gen
+| G_LTAC2_for_each_goal ltac2_for_each_goal
 | G_LTAC2_tactic_then_last ltac2_tactic_then_last
 | G_LTAC2_as_name ltac2_as_name
 | G_LTAC2_as_ipat ltac2_as_ipat
@@ -94,18 +94,22 @@ RENAME: [
 | G_LTAC2_match_list ltac2_match_list
 ]
 
-(* renames to eliminate qualified names
-   put other renames at the end *)
+(* Renames to eliminate qualified names.
+   Put other renames at the end *)
 RENAME: [
   (* map missing names for rhs *)
 | Constr.constr term
 | Constr.global global
 | Constr.lconstr lconstr
-| Constr.lconstr_pattern cpattern
+| Constr.cpattern cpattern
 | G_vernac.query_command query_command
 | G_vernac.section_subset_expr section_var_expr
 | Prim.ident ident
 | Prim.reference reference
+| Prim.string string
+| Prim.integer integer
+| Prim.qualid qualid
+| Prim.natural natural
 | Pvernac.Vernac_.main_entry vernac_control
 | Tactic.tactic tactic
 
@@ -117,7 +121,7 @@ RENAME: [
 | Prim.identref ident
 | Prim.natural natural
 *)
-| Vernac.rec_definition rec_definition
+| Vernac.fix_definition fix_definition
 (* todo: hmm, rename adds 1 prodn to closed_binder?? *)
 | Constr.closed_binder closed_binder
 ]
@@ -183,19 +187,19 @@ DELETE: [
 (* additional nts to be spliced *)
 
 tactic_then_last: [
-| REPLACE "|" LIST0 ( OPT tactic_expr5 ) SEP "|"
-| WITH LIST0 ( "|" ( OPT tactic_expr5 ) )
+| REPLACE "|" LIST0 ( OPT ltac_expr5 ) SEP "|"
+| WITH LIST0 ( "|" ( OPT ltac_expr5 ) )
 ]
 
 goal_tactics: [
-| LIST0 ( OPT tactic_expr5 ) SEP "|"
+| LIST0 ( OPT ltac_expr5 ) SEP "|"
 ]
 
-tactic_then_gen: [ | DELETENT ]
+for_each_goal: [ | DELETENT ]
 
-tactic_then_gen: [
+for_each_goal: [
 | goal_tactics
-| OPT ( goal_tactics "|" ) OPT tactic_expr5 ".." OPT ( "|" goal_tactics )
+| OPT ( goal_tactics "|" ) OPT ltac_expr5 ".." OPT ( "|" goal_tactics )
 ]
 
 tactic_then_last: [
@@ -203,19 +207,19 @@ tactic_then_last: [
 ]
 
 ltac2_tactic_then_last: [
-| REPLACE "|" LIST0 ( OPT tac2expr6 ) SEP "|"      (* Ltac2 plugin *)
-| WITH LIST0 (  "|" OPT tac2expr6 )  TAG Ltac2
+| REPLACE "|" LIST0 ( OPT ltac2_expr6 ) SEP "|"      (* Ltac2 plugin *)
+| WITH LIST0 (  "|" OPT ltac2_expr6 )  TAG Ltac2
 ]
 
 ltac2_goal_tactics: [
-| LIST0 ( OPT tac2expr6 ) SEP "|"  TAG Ltac2
+| LIST0 ( OPT ltac2_expr6 ) SEP "|"  TAG Ltac2
 ]
 
-ltac2_tactic_then_gen: [ | DELETENT ]
+ltac2_for_each_goal: [ | DELETENT ]
 
-ltac2_tactic_then_gen: [
+ltac2_for_each_goal: [
 | ltac2_goal_tactics  TAG Ltac2
-| OPT ( ltac2_goal_tactics "|" ) OPT tac2expr6 ".." OPT ( "|" ltac2_goal_tactics )  TAG Ltac2
+| OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr6 ".." OPT ( "|" ltac2_goal_tactics )  TAG Ltac2
 ]
 
 ltac2_tactic_then_last: [
@@ -257,45 +261,40 @@ let_type_cstr: [
 | type_cstr
 ]
 
-(* rename here because we want to use "return_type" for something else *)
-RENAME: [
-| return_type as_return_type
-]
-
 case_item: [
-| REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
-| WITH operconstr100 OPT ("as" name) OPT [ "in" pattern200 ]
+| REPLACE term100 OPT [ "as" name ] OPT [ "in" pattern200 ]
+| WITH term100 OPT ("as" name) OPT [ "in" pattern200 ]
 ]
 
 binder_constr: [
-| MOVETO term_forall_or_fun "forall" open_binders "," operconstr200
-| MOVETO term_forall_or_fun "fun" open_binders "=>" operconstr200
-| MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
-| MOVETO term_if "if" operconstr200 as_return_type "then" operconstr200 "else" operconstr200
-| MOVETO term_fix "let" "fix" fix_decl "in" operconstr200
-| MOVETO term_cofix "let" "cofix" cofix_decl "in" operconstr200
-| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200
-| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
-| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
-| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| MOVETO term_forall_or_fun "forall" open_binders "," term200
+| MOVETO term_forall_or_fun "fun" open_binders "=>" term200
+| MOVETO term_let "let" name binders let_type_cstr ":=" term200 "in" term200
+| MOVETO term_if "if" term200 as_return_type "then" term200 "else" term200
+| MOVETO term_fix "let" "fix" fix_decl "in" term200
+| MOVETO term_cofix "let" "cofix" cofix_body "in" term200
+| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
+| MOVETO term_let "let" "'" pattern200 ":=" term200 "in" term200
+| MOVETO term_let "let" "'" pattern200 ":=" term200 case_type "in" term200
+| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
 | MOVETO term_fix "fix" fix_decls
 | MOVETO term_cofix "cofix" cofix_decls
 ]
 
 term_let: [
-| REPLACE "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
-| WITH "let" name let_type_cstr ":=" operconstr200 "in" operconstr200
-| "let" name LIST1 binder let_type_cstr ":=" operconstr200 "in" operconstr200
+| REPLACE "let" name binders let_type_cstr ":=" term200 "in" term200
+| WITH "let" name let_type_cstr ":=" term200 "in" term200
+| "let" name LIST1 binder let_type_cstr ":=" term200 "in" term200
 (* Don't need to document that "( )" is equivalent to "()" *)
-| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200
-| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" operconstr200 "in" operconstr200
-| REPLACE "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
-| WITH  "let" "'" pattern200 ":=" operconstr200 OPT case_type "in" operconstr200
-| DELETE "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
+| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200
+| REPLACE "let" "'" pattern200 ":=" term200 "in" term200
+| WITH  "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
+| DELETE "let" "'" pattern200 ":=" term200 case_type "in" term200
 ]
 
 atomic_constr: [
-| MOVETO qualid_annotated global univ_instance
+| MOVETO qualid_annotated global univ_annot
 | MOVETO primitive_notations NUMBER
 | MOVETO primitive_notations string
 | MOVETO term_evar "_"
@@ -308,9 +307,9 @@ atomic_constr: [
 | MOVETO term_evar pattern_ident evar_instance
 ]
 
-tactic_expr0: [
-| REPLACE "[" ">" tactic_then_gen "]"
-| WITH "[>" tactic_then_gen "]"
+ltac_expr0: [
+| REPLACE "[" ">" for_each_goal "]"
+| WITH "[>" for_each_goal "]"
 ]
 
 (* lexer token *)
@@ -337,68 +336,68 @@ scope_delimiter: [
 ]
 
 type: [
-| operconstr200
+| term200
 ]
 
-operconstr100: [
-| REPLACE operconstr99 "<:" operconstr200
-| WITH operconstr99 "<:" type
-| MOVETO term_cast operconstr99 "<:" type
-| REPLACE operconstr99 "<<:" operconstr200
-| WITH operconstr99 "<<:" type
-| MOVETO term_cast operconstr99 "<<:" type
-| REPLACE operconstr99 ":" operconstr200
-| WITH operconstr99 ":" type
-| MOVETO term_cast operconstr99 ":" type
-| MOVETO term_cast operconstr99 ":>"
+term100: [
+| REPLACE term99 "<:" term200
+| WITH term99 "<:" type
+| MOVETO term_cast term99 "<:" type
+| REPLACE term99 "<<:" term200
+| WITH term99 "<<:" type
+| MOVETO term_cast term99 "<<:" type
+| REPLACE term99 ":" term200
+| WITH term99 ":" type
+| MOVETO term_cast term99 ":" type
+| MOVETO term_cast term99 ":>"
 ]
 
 constr: [
-| REPLACE "@" global univ_instance
+| REPLACE "@" global univ_annot
 | WITH "@" qualid_annotated
 | MOVETO term_explicit "@" qualid_annotated
 ]
 
-operconstr10: [
+term10: [
 (* Separate this LIST0 in the nonempty and the empty case *)
 (* The empty case is covered by constr *)
-| REPLACE "@" global univ_instance LIST0 operconstr9
-| WITH "@" qualid_annotated LIST1 operconstr9
-| REPLACE operconstr9
+| REPLACE "@" global univ_annot LIST0 term9
+| WITH "@" qualid_annotated LIST1 term9
+| REPLACE term9
 | WITH constr
-| MOVETO term_application operconstr9 LIST1 appl_arg
-| MOVETO term_application "@" qualid_annotated LIST1 operconstr9
+| MOVETO term_application term9 LIST1 arg
+| MOVETO term_application "@" qualid_annotated LIST1 term9
 (* fixme: add in as a prodn somewhere *)
 | MOVETO dangling_pattern_extension_rule "@" pattern_ident LIST1 identref
 | DELETE dangling_pattern_extension_rule
 ]
 
-operconstr9: [
+term9: [
 (* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
-| DELETE ".." operconstr0 ".."
+| DELETE ".." term0 ".."
 ]
 
-operconstr1: [
-| REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
-| WITH    operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *)
-| REPLACE operconstr0 "%" IDENT
-| WITH operconstr0 "%" scope_key
-| MOVETO term_scope operconstr0 "%" scope_key
-| MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")"
-| MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
+term1: [
+| REPLACE term0 ".(" global LIST0 arg ")"
+| WITH    term0 ".(" global LIST0 arg ")" (* huh? *)
+| REPLACE term0 "%" IDENT
+| WITH term0 "%" scope_key
+| MOVETO term_scope term0 "%" scope_key
+| MOVETO term_projection term0 ".(" global LIST0 arg ")"
+| MOVETO term_projection term0 ".(" "@" global LIST0 ( term9 ) ")"
 ]
 
-operconstr0: [
+term0: [
 (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
 | DELETE "{" binder_constr "}"
 | REPLACE "{|" record_declaration bar_cbrace
 | WITH "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
 | MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
-| MOVETO term_generalizing "`{" operconstr200 "}"
-| MOVETO term_generalizing "`(" operconstr200 ")"
-| MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
-| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_instance
-| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_instance
+| MOVETO term_generalizing "`{" term200 "}"
+| MOVETO term_generalizing "`(" term200 ")"
+| MOVETO term_ltac "ltac" ":" "(" ltac_expr5 ")"
+| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_annot
+| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_annot
 ]
 
 fix_decls: [
@@ -408,9 +407,9 @@ fix_decls: [
 ]
 
 cofix_decls: [
-| DELETE cofix_decl
-| REPLACE cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref
-| WITH cofix_decl OPT ( LIST1 ( "with" cofix_decl ) "for" identref )
+| DELETE cofix_body
+| REPLACE cofix_body "with" LIST1 cofix_body SEP "with" "for" identref
+| WITH cofix_body OPT ( LIST1 ( "with" cofix_body ) "for" identref )
 ]
 
 fields_def: [
@@ -481,11 +480,11 @@ name_colon: [
 ]
 
 typeclass_constraint: [
-| EDIT ADD_OPT "!" operconstr200
-| REPLACE "{" name "}" ":" [ "!" | ] operconstr200
-| WITH "{" name "}" ":" OPT "!"  operconstr200
-| REPLACE name ":" [ "!" | ] operconstr200
-| WITH name ":" OPT "!" operconstr200
+| EDIT ADD_OPT "!" term200
+| REPLACE "{" name "}" ":" [ "!" | ] term200
+| WITH "{" name "}" ":" OPT "!"  term200
+| REPLACE name ":" [ "!" | ] term200
+| WITH name ":" OPT "!" term200
 ]
 
 (* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*)
@@ -566,14 +565,14 @@ gallina: [
 |   [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition )
 |   "Class" record_definition
 |   "Class" singleton_class_definition
-| REPLACE "Fixpoint" LIST1 rec_definition SEP "with"
-| WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
-| REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with"
-| WITH "Let" "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
-| REPLACE "CoFixpoint" LIST1 corec_definition SEP "with"
-| WITH "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
-| REPLACE "Let" "CoFixpoint" LIST1 corec_definition SEP "with"
-| WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
+| REPLACE "Fixpoint" LIST1 fix_definition SEP "with"
+| WITH "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
+| REPLACE "Let" "Fixpoint" LIST1 fix_definition SEP "with"
+| WITH "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
+| REPLACE "CoFixpoint" LIST1 cofix_definition SEP "with"
+| WITH "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
+| REPLACE "Let" "CoFixpoint" LIST1 cofix_definition SEP "with"
+| WITH "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
 | REPLACE "Scheme" LIST1 scheme SEP "with"
 | WITH "Scheme" scheme LIST0 ( "with" scheme )
 ]
@@ -582,7 +581,7 @@ finite_token: [
 | DELETENT
 ]
 
-constructor_list_or_record_decl: [
+constructors_or_record: [
 | OPTINREF
 ]
 
@@ -604,7 +603,7 @@ inline: [
 | OPTINREF
 ]
 
-univ_instance: [
+univ_annot: [
 | OPTINREF
 ]
 
@@ -613,15 +612,15 @@ univ_decl: [
 | WITH    "@{" LIST0 identref  OPT "+"  OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
 ]
 
-of_type_with_opt_coercion: [
+of_type: [
 | DELETENT
 ]
 
-of_type_with_opt_coercion: [
+of_type: [
 | [ ":" | ":>" ] type
 ]
 
-attribute_value: [
+attr_value: [
 | OPTINREF
 ]
 
@@ -657,14 +656,6 @@ ltac2_branches: [
 | OPTINREF
 ]
 
-RENAME: [
-| red_flag ltac2_red_flag
-| red_flags red_flag
-]
-
-RENAME: [
-]
-
 strategy_flag: [
 | REPLACE OPT delta_flag
 | WITH delta_flag
@@ -697,8 +688,8 @@ is_module_type: [
 ]
 
 gallina_ext: [
-| REPLACE "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
-| WITH "Arguments" smart_global LIST0 argument_spec_block    LIST0 [  "," LIST0 more_implicits_block ]                OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| REPLACE "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ]
+| WITH "Arguments" smart_global LIST0 arg_specs    LIST0 [  "," LIST0 implicits_alt ]                OPT [ ":" LIST1 args_modifier SEP "," ]
 | REPLACE "Implicit" "Type" reserv_list
 | WITH "Implicit" [ "Type" | "Types" ] reserv_list
 | DELETE "Implicit" "Types" reserv_list
@@ -727,11 +718,11 @@ gallina_ext: [
 | WITH "Generalizable" [  [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ]
 
 (* don't show Export for Set, Unset *)
-| REPLACE "Export" "Set" option_table option_setting
-| WITH "Set" option_table option_setting
-| REPLACE "Export" "Unset" option_table
-| WITH "Unset" option_table
-| REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
+| REPLACE "Export" "Set" setting_name option_setting
+| WITH "Set" setting_name option_setting
+| REPLACE "Export" "Unset" setting_name
+| WITH "Unset" setting_name
+| REPLACE "Instance" instance_name ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
 | WITH "Instance" instance_name ":" type hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ]
 
 | REPLACE "From" global "Require" export_token LIST1 global
@@ -822,92 +813,92 @@ DELETE: [
 | tactic_then_locality
 ]
 
-tactic_expr5: [
-(* make these look consistent with use of binder_tactic in other tactic_expr* *)
+ltac_expr5: [
+(* make these look consistent with use of binder_tactic in other ltac_expr* *)
 | DELETE binder_tactic
-| DELETE tactic_expr4
-| [ tactic_expr4 | binder_tactic ]
+| DELETE ltac_expr4
+| [ ltac_expr4 | binder_tactic ]
 ]
 
 ltac_constructs: [
 (* repeated in main ltac grammar - need to create a COPY edit *)
-| tactic_expr3 ";" [ tactic_expr3 | binder_tactic ]
-| tactic_expr3 ";" "[" tactic_then_gen "]"
+| ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
+| ltac_expr3 ";" "[" for_each_goal "]"
 
-| tactic_expr1 "+" [ tactic_expr2 | binder_tactic ]
-| tactic_expr1 "||" [ tactic_expr2 | binder_tactic ]
+| ltac_expr1 "+" [ ltac_expr2 | binder_tactic ]
+| ltac_expr1 "||" [ ltac_expr2 | binder_tactic ]
 
-(* | qualid LIST0 tactic_arg  add later due renaming tactic_arg *)
+(* | qualid LIST0 tactic_value  add later due renaming tactic_value *)
 
-| "[>" tactic_then_gen "]"
-| toplevel_selector tactic_expr5
+| "[>" for_each_goal "]"
+| toplevel_selector ltac_expr5
 ]
 
-tactic_expr4: [
-| REPLACE tactic_expr3 ";" tactic_then_gen "]"
-| WITH tactic_expr3 ";" "[" tactic_then_gen "]"
-| REPLACE tactic_expr3 ";" binder_tactic
-| WITH tactic_expr3 ";" [ tactic_expr3 | binder_tactic ]
-| DELETE tactic_expr3 ";" tactic_expr3
+ltac_expr4: [
+| REPLACE ltac_expr3 ";" for_each_goal "]"
+| WITH ltac_expr3 ";" "[" for_each_goal "]"
+| REPLACE ltac_expr3 ";" binder_tactic
+| WITH ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
+| DELETE ltac_expr3 ";" ltac_expr3
 ]
 
 l3_tactic: [ ]
 
-tactic_expr3: [
-| DELETE "abstract" tactic_expr2
-| REPLACE "abstract" tactic_expr2 "using" ident
-| WITH "abstract" tactic_expr2 OPT ( "using" ident )
+ltac_expr3: [
+| DELETE "abstract" ltac_expr2
+| REPLACE "abstract" ltac_expr2 "using" ident
+| WITH "abstract" ltac_expr2 OPT ( "using" ident )
 | l3_tactic
 | MOVEALLBUT ltac_builtins
 | l3_tactic
-| tactic_expr2
+| ltac_expr2
 ]
 
 l2_tactic: [ ]
 
-tactic_expr2: [
-| REPLACE tactic_expr1 "+" binder_tactic
-| WITH tactic_expr1 "+"  [ tactic_expr2 | binder_tactic ]
-| DELETE tactic_expr1 "+" tactic_expr2
-| REPLACE tactic_expr1 "||" binder_tactic
-| WITH tactic_expr1 "||" [ tactic_expr2 | binder_tactic ]
-| DELETE tactic_expr1 "||" tactic_expr2
-| MOVETO ltac_builtins "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2
+ltac_expr2: [
+| REPLACE ltac_expr1 "+" binder_tactic
+| WITH ltac_expr1 "+"  [ ltac_expr2 | binder_tactic ]
+| DELETE ltac_expr1 "+" ltac_expr2
+| REPLACE ltac_expr1 "||" binder_tactic
+| WITH ltac_expr1 "||" [ ltac_expr2 | binder_tactic ]
+| DELETE ltac_expr1 "||" ltac_expr2
+| MOVETO ltac_builtins "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2
 | l2_tactic
 | DELETE ltac_builtins
 ]
 
 l1_tactic: [ ]
 
-tactic_expr1: [
+ltac_expr1: [
 | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO simple_tactic match_key OPT "reverse" "goal" "with" match_context_list "end"
-| MOVETO simple_tactic match_key tactic_expr5 "with" match_list "end"
+| MOVETO simple_tactic match_key ltac_expr5 "with" match_list "end"
 | REPLACE failkw [ int_or_var | ] LIST0 message_token
 | WITH failkw OPT int_or_var LIST0 message_token
-| REPLACE reference LIST0 tactic_arg_compat
-| WITH reference LIST1 tactic_arg_compat
+| REPLACE reference LIST0 tactic_arg
+| WITH reference LIST1 tactic_arg
 | l1_tactic
 | DELETE simple_tactic
 | MOVEALLBUT ltac_builtins
 | l1_tactic
-| tactic_arg
-| reference LIST1 tactic_arg_compat
-| tactic_expr0
+| tactic_value
+| reference LIST1 tactic_arg
+| ltac_expr0
 ]
 
 (* split match_context_rule *)
 goal_pattern: [
-| LIST0 match_hyps SEP "," "|-" match_pattern
-| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]"
+| LIST0 match_hyp SEP "," "|-" match_pattern
+| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]"
 | "_"
 ]
 
 match_context_rule: [
-| DELETE LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5
-| DELETE "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5
-| DELETE "_" "=>" tactic_expr5
-| goal_pattern "=>" tactic_expr5
+| DELETE LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr5
+| DELETE "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr5
+| DELETE "_" "=>" ltac_expr5
+| goal_pattern "=>" ltac_expr5
 ]
 
 match_context_list: [
@@ -920,10 +911,10 @@ match_list: [
 
 match_rule: [
 (* redundant; match_pattern -> term -> _ *)
-| DELETE "_" "=>" tactic_expr5
+| DELETE "_" "=>" ltac_expr5
 ]
 
-selector_body: [
+selector: [
 | REPLACE range_selector_or_nth  (* depends on whether range_selector_or_nth is deleted first *)
 | WITH LIST1 range_selector SEP ","
 ]
@@ -1091,7 +1082,7 @@ simple_tactic: [
 | EDIT "psatz_Q" ADD_OPT int_or_var tactic
 | EDIT "psatz_Z" ADD_OPT int_or_var tactic
 | REPLACE "subst" LIST1 hyp
-| WITH "subst" OPT ( LIST1 hyp )
+| WITH "subst" LIST0 hyp
 | DELETE "subst"
 | DELETE "congruence"
 | DELETE "congruence" natural
@@ -1102,18 +1093,18 @@ simple_tactic: [
 | REPLACE "show" "ltac" "profile" "cutoff" integer
 | WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ]
 | DELETE "show" "ltac" "profile" string
-(* perversely, the mlg uses "tactic3" instead of "tactic_expr3" *)
+(* perversely, the mlg uses "tactic3" instead of "ltac_expr3" *)
 | DELETE "transparent_abstract" tactic3
 | REPLACE "transparent_abstract" tactic3 "using" ident
-| WITH "transparent_abstract" tactic_expr3 OPT ( "using" ident )
-| REPLACE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
-| WITH "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident )
+| WITH "transparent_abstract" ltac_expr3 OPT ( "using" ident )
+| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident )
+| DELETE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
 | DELETE "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident
 | DELETE "typeclasses" "eauto" "bfs" OPT int_or_var
 | DELETE "typeclasses" "eauto" OPT int_or_var
 (* in Tactic Notation: *)
 | "setoid_replace" constr "with" constr OPT ( "using" "relation" constr ) OPT ( "in" hyp )
-       OPT ( "at" LIST1 int_or_var ) OPT ( "by" tactic_expr3 )
+       OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 )
 ]
 
 (* todo: don't use DELETENT for this *)
@@ -1168,8 +1159,8 @@ command: [
 | "SubClass" ident_decl def_body
 | REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with"
 | WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body )
-| REPLACE "Function" LIST1 function_rec_definition_loc SEP "with"      (* funind plugin *)
-| WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc )      (* funind plugin *)
+| REPLACE "Function" LIST1 function_fix_definition SEP "with"      (* funind plugin *)
+| WITH "Function" function_fix_definition LIST0 ( "with" function_fix_definition )      (* 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"
@@ -1180,16 +1171,16 @@ command: [
 | WITH "Back" OPT natural
 | REPLACE "Load" [ "Verbose" | ] [ ne_string | IDENT ]
 | WITH "Load" OPT "Verbose" [ ne_string | IDENT ]
-| DELETE "Unset" option_table
-| REPLACE "Set" option_table option_setting
-| WITH OPT "Export" "Set" option_table   (* set flag *)
-| REPLACE "Test" option_table "for" LIST1 table_value
-| WITH "Test" option_table OPT ( "for" LIST1 table_value )
-| DELETE "Test" option_table
+| DELETE "Unset" setting_name
+| REPLACE "Set" setting_name option_setting
+| WITH OPT "Export" "Set" setting_name   (* set flag *)
+| REPLACE "Test" setting_name "for" LIST1 table_value
+| WITH "Test" setting_name OPT ( "for" LIST1 table_value )
+| DELETE "Test" setting_name
 
 (* hide the fact that table names are limited to 2 IDENTs *)
 | REPLACE "Add" IDENT IDENT LIST1 table_value
-| WITH "Add" option_table LIST1 table_value
+| WITH "Add" setting_name LIST1 table_value
 | DELETE "Add" IDENT LIST1 table_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
@@ -1247,7 +1238,7 @@ command: [
 
 (* hide the fact that table names are limited to 2 IDENTs *)
 | REPLACE "Remove" IDENT IDENT LIST1 table_value
-| WITH "Remove" option_table LIST1 table_value
+| WITH "Remove" setting_name LIST1 table_value
 | DELETE "Remove" IDENT LIST1 table_value
 | DELETE "Restore" "State" IDENT
 | DELETE "Restore" "State" ne_string
@@ -1294,10 +1285,10 @@ command: [
 | WITH "Declare" "Scope" scope_name
 
 (* odd that these are in command while other notation-related ones are in syntax *)
-| REPLACE "Numeral" "Notation" reference reference reference ":" ident numnotoption
-| WITH "Numeral" "Notation" reference reference reference ":" scope_name numnotoption
-| REPLACE "Number" "Notation" reference reference reference ":" ident numnotoption
-| WITH "Number" "Notation" reference reference reference ":" scope_name numnotoption
+| REPLACE "Numeral" "Notation" reference reference reference ":" ident numeral_modifier
+| WITH "Numeral" "Notation" reference reference reference ":" scope_name numeral_modifier
+| REPLACE "Number" "Notation" reference reference reference ":" ident numeral_modifier
+| WITH "Number" "Notation" reference reference reference ":" scope_name numeral_modifier
 | REPLACE "String" "Notation" reference reference reference ":" ident
 | WITH "String" "Notation" reference reference reference ":" scope_name
 
@@ -1357,7 +1348,7 @@ syntax_modifier: [
 | WITH LIST1 IDENT SEP "," "at" level
 ]
 
-syntax_extension_type: [
+explicit_subentry: [
 | REPLACE "strict" "pattern" "at" "level" natural
 | WITH "strict" "pattern" OPT ( "at" "level" natural )
 | DELETE "strict" "pattern"
@@ -1367,31 +1358,31 @@ syntax_extension_type: [
 | DELETE "constr"    (* covered by another prod *)
 ]
 
-numnotoption: [
+numeral_modifier: [
 | OPTINREF
 ]
 
 binder_tactic: [
-| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
-| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5
+| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
+| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5
 | MOVEALLBUT ltac_builtins
 ]
 
-record_binder_body: [
-| REPLACE binders of_type_with_opt_coercion lconstr
-| WITH binders of_type_with_opt_coercion
-| REPLACE binders of_type_with_opt_coercion lconstr ":=" lconstr
-| WITH binders of_type_with_opt_coercion ":=" lconstr
+field_body: [
+| REPLACE binders of_type lconstr
+| WITH binders of_type
+| REPLACE binders of_type lconstr ":=" lconstr
+| WITH binders of_type ":=" lconstr
 ]
 
-simple_assum_coe: [
-| REPLACE LIST1 ident_decl of_type_with_opt_coercion lconstr
-| WITH LIST1 ident_decl of_type_with_opt_coercion
+assumpt: [
+| REPLACE LIST1 ident_decl of_type lconstr
+| WITH LIST1 ident_decl of_type
 ]
 
 constructor_type: [
-| REPLACE binders [ of_type_with_opt_coercion lconstr | ]
-| WITH binders OPT of_type_with_opt_coercion
+| REPLACE binders [ of_type lconstr | ]
+| WITH binders OPT of_type
 ]
 
 (* todo: is this really correct? Search for "Pvernac.register_proof_mode" *)
@@ -1435,12 +1426,12 @@ legacy_attr: [
 
 sentence: [ ]  (* productions defined below *)
 
-rec_definition: [
+fix_definition: [
 | REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
 | WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
 
-corec_definition: [
+cofix_definition: [
 | REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
 | WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
@@ -1457,7 +1448,7 @@ inductive_definition: [
 ]
 
 (* note that constructor -> identref constructor_type *)
-constructor_list_or_record_decl: [
+constructors_or_record: [
 | DELETE "|" LIST1 constructor SEP "|"
 | REPLACE identref constructor_type "|" LIST1 constructor SEP "|"
 | WITH OPT "|" LIST1 constructor SEP "|"
@@ -1468,8 +1459,8 @@ constructor_list_or_record_decl: [
 ]
 
 record_binder: [
-| REPLACE name record_binder_body
-| WITH name OPT record_binder_body
+| REPLACE name field_body
+| WITH name OPT field_body
 | DELETE name
 ]
 
@@ -1636,7 +1627,7 @@ ltac2_rewriter: [
 | OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings
 ]
 
-tac2expr0: [
+ltac2_expr0: [
 | DELETE "(" ")"
 ]
 
@@ -1813,9 +1804,9 @@ input_fun: [
 ]
 
 let_clause: [
-| DELETE identref ":=" tactic_expr5
-| REPLACE "_" ":=" tactic_expr5
-| WITH name  ":=" tactic_expr5
+| DELETE identref ":=" ltac_expr5
+| REPLACE "_" ":=" ltac_expr5
+| WITH name  ":=" ltac_expr5
 ]
 
 tactic_mode: [
@@ -1837,11 +1828,11 @@ tactic_mode: [
 
 tactic_mode: [ | DELETENT ]
 
-sexpr: [
+ltac2_scope: [
 | REPLACE syn_node      (* Ltac2 plugin *)
 | WITH name TAG Ltac2
-| REPLACE syn_node "(" LIST1 sexpr SEP "," ")"      (* Ltac2 plugin *)
-| WITH name "(" LIST1 sexpr SEP "," ")" TAG Ltac2
+| REPLACE syn_node "(" LIST1 ltac2_scope SEP "," ")"      (* Ltac2 plugin *)
+| WITH name "(" LIST1 ltac2_scope SEP "," ")" TAG Ltac2
 ]
 
 syn_node: [ | DELETENT ]
@@ -1851,7 +1842,7 @@ RENAME: [
 ]
 
 toplevel_selector: [
-| selector_body
+| selector
 | "all"
 | "!"
 (* par is accepted even though it's not in the .mlg *)
@@ -1859,7 +1850,7 @@ toplevel_selector: [
 ]
 
 toplevel_selector_temp: [
-| DELETE selector_body ":"
+| DELETE selector ":"
 | DELETE "all" ":"
 | DELETE "!" ":"
 | toplevel_selector ":"
@@ -1900,7 +1891,7 @@ query_command: [ ] (* re-add as a placeholder *)
 sentence: [
 | OPT attributes command "."
 | OPT attributes OPT ( natural ":" ) query_command "."
-| OPT attributes OPT ( toplevel_selector ":" ) tactic_expr5 [ "." | "..." ]
+| OPT attributes OPT ( toplevel_selector ":" ) ltac_expr5 [ "." | "..." ]
 | control_command
 ]
 
@@ -1924,18 +1915,18 @@ ltac_defined_tactics: [
 | "split_Rabs"
 | "split_Rmult"
 | "tauto"
-| "time_constr" tactic_expr5
+| "time_constr" ltac_expr5
 | "zify"
 ]
 
 (* todo: need careful review; assume that "[" ... "]" are literals *)
 tactic_notation_tactics: [
-| "assert_fails" tactic_expr3
-| "assert_succeeds" tactic_expr3
+| "assert_fails" ltac_expr3
+| "assert_succeeds" ltac_expr3
 | "field" OPT ( "[" LIST1 constr "]" )
 | "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident )
 | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident )
-| "intuition" OPT tactic_expr5
+| "intuition" OPT ltac_expr5
 | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr )
 | "psatz" constr OPT int_or_var
 | "ring" OPT ( "[" LIST1 constr "]" )
@@ -1943,8 +1934,8 @@ tactic_notation_tactics: [
 ]
 
 (* defined in OCaml outside of mlgs *)
-tactic_arg: [
-| "uconstr" ":" "(" operconstr200 ")"
+tactic_value: [
+| "uconstr" ":" "(" term200 ")"
 | MOVEALLBUT simple_tactic
 ]
 
@@ -1952,10 +1943,6 @@ nonterminal: [ ]
 
 value_tactic: [ ]
 
-RENAME: [
-| tactic_arg tactic_value
-]
-
 syn_value: [
 | IDENT; ":" "(" nonterminal ")"
 ]
@@ -1974,8 +1961,8 @@ ltac2_match_key: [
 ]
 
 ltac2_constructs: [
-| ltac2_match_key tac2expr6 "with" ltac2_match_list "end"
-| ltac2_match_key OPT "reverse" "goal" "with" gmatch_list "end"
+| ltac2_match_key ltac2_expr6 "with" ltac2_match_list "end"
+| ltac2_match_key OPT "reverse" "goal" "with" goal_match_list "end"
 ]
 
 simple_tactic: [
@@ -1987,9 +1974,9 @@ simple_tactic: [
 ]
 
 tacdef_body: [
-| REPLACE global LIST1 input_fun ltac_def_kind tactic_expr5
-| WITH global LIST0 input_fun ltac_def_kind tactic_expr5
-| DELETE global ltac_def_kind tactic_expr5
+| REPLACE global LIST1 input_fun ltac_def_kind ltac_expr5
+| WITH global LIST0 input_fun ltac_def_kind ltac_expr5
+| DELETE global ltac_def_kind ltac_expr5
 ]
 
 tac2def_typ: [
@@ -2071,7 +2058,7 @@ atomic_tac2pat: [
 | OPTINREF
 ]
 
-tac2expr0: [
+ltac2_expr0: [
 (*
 | DELETE "(" ")" (* covered by "()" prodn *)
 | REPLACE "{" [  | LIST1 tac2rec_fieldexpr OPT ";" ] "}"
@@ -2084,13 +2071,13 @@ tac2expr0: [
 use LIST1? *)
 
 SPLICE: [
-| tac2expr4
+| ltac2_expr4
 ]
 
-tac2expr3: [
-| REPLACE tac2expr2 "," LIST1 tac2expr2 SEP ","      (* Ltac2 plugin *)
-| WITH LIST1 tac2expr2 SEP "," TAG Ltac2
-| DELETE tac2expr2      (* Ltac2 plugin *)
+ltac2_expr3: [
+| REPLACE ltac2_expr2 "," LIST1 ltac2_expr2 SEP ","      (* Ltac2 plugin *)
+| WITH LIST1 ltac2_expr2 SEP "," TAG Ltac2
+| DELETE ltac2_expr2      (* Ltac2 plugin *)
 ]
 
 tac2rec_fieldexprs: [
@@ -2171,7 +2158,7 @@ ltac2_entry: [
 | WITH "Ltac2" tac2def_val
 | REPLACE tac2def_ext     (* Ltac2 plugin *)
 | WITH "Ltac2" tac2def_ext
-| "Ltac2" "Notation" [ string | lident ] ":=" tac2expr6 TAG Ltac2  (* variant *)
+| "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr6 TAG Ltac2  (* variant *)
 | MOVEALLBUT command
 (* todo: MOVEALLBUT should ignore tag on "but" prodns *)
 ]
@@ -2207,21 +2194,14 @@ SPLICE: [
 | anti
 ]
 
-tac2expr5: [
-| REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" tac2expr6      (* Ltac2 plugin *)
-| WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" tac2expr6 TAG Ltac2
-| MOVETO simple_tactic "match" tac2expr5 "with" OPT ltac2_branches "end"      (* Ltac2 plugin *)
+ltac2_expr5: [
+| REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6      (* Ltac2 plugin *)
+| WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2
+| MOVETO simple_tactic "match" ltac2_expr5 "with" OPT ltac2_branches "end"      (* Ltac2 plugin *)
 | DELETE simple_tactic
 ]
 
-RENAME: [
-| Prim.string string
-| Prim.integer integer
-| Prim.qualid qualid
-| Prim.natural natural
-]
-
-gmatch_list: [
+goal_match_list: [
 | EDIT ADD_OPT "|" LIST1 gmatch_rule SEP "|"      (* Ltac2 plugin *)
 ]
 
@@ -2290,6 +2270,10 @@ subprf: [
 | "{" (* should be removed.  See https://github.com/coq/coq/issues/12004 *)
 ]
 
+ltac2_expr: [
+| DELETE _ltac2_expr
+]
+
 SPLICE: [
 | clause
 | noedit_mode
@@ -2309,10 +2293,10 @@ SPLICE: [
 | ltac_selector
 | Constr.ident
 | attribute_list
-| operconstr99
-| operconstr90
-| operconstr9
-| operconstr8
+| term99
+| term90
+| term9
+| term8
 | pattern200
 | pattern99
 | pattern90
@@ -2363,7 +2347,7 @@ SPLICE: [
 | check_module_types
 | constr_pattern
 | decl_sep
-| function_rec_definition_loc (* loses funind annotation *)
+| function_fix_definition (* loses funind annotation *)
 | glob
 | glob_constr_with_bindings
 | id_or_meta
@@ -2381,7 +2365,6 @@ SPLICE: [
 | decorated_vernac
 | ext_module_expr
 | ext_module_type
-| pattern_ident
 | test
 | binder_constr
 | atomic_constr
@@ -2449,7 +2432,6 @@ SPLICE: [
 | intropatterns
 | instance_name
 | failkw
-| selector
 | ne_in_or_out_modules
 | search_queries
 | locatable
@@ -2472,7 +2454,6 @@ SPLICE: [
 | refglobals (* Ltac2 *)
 | syntax_modifiers
 | array_elems
-| ltac2_expr
 | G_LTAC2_input_fun
 | ltac2_simple_intropattern_closed
 | ltac2_with_bindings
@@ -2489,81 +2470,33 @@ RENAME: [
 | tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
 | tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
 | tactic0 ltac_expr0  (* todo: can't figure out how this gets mapped by coqpp *)
-| ltac1_expr ltac_expr
-| tactic_expr5 ltac_expr
-| tactic_expr4 ltac_expr4
-| tactic_expr3 ltac_expr3
-| tactic_expr2 ltac_expr2
-| tactic_expr1 ltac_expr1
-| tactic_expr0 ltac_expr0
+| ltac_expr5 ltac_expr
 
 (* | nonsimple_intropattern intropattern (* ltac2 *) *)
 
-| operconstr200 term   (* historical name *)
-| operconstr100 term100
-| operconstr10 term10
-| operconstr1 term1
-| operconstr0 term0
+| term200 term
 | pattern100 pattern
-| match_constr term_match
 (*| impl_ident_tail impl_ident*)
 | ssexpr50 section_var_expr50
 | ssexpr0 section_var_expr0
 | section_subset_expr section_var_expr
 | fun_scheme_arg func_scheme_def
 
-| tactic_then_gen for_each_goal
-| ltac2_tactic_then_gen ltac2_for_each_goal
-| selector_body selector
-| match_hyps match_hyp
-
 | BULLET bullet
-| fix_decl fix_body
-| cofix_decl cofix_body
-(* todo: it's confusing that Constr.constr and constr mean different things *)
-| constr one_term
-| appl_arg arg
-| rec_definition fix_definition
-| corec_definition cofix_definition
-| univ_instance univ_annot
-| simple_assum_coe assumpt
-| of_type_with_opt_coercion of_type
-| attribute_value attr_value
-| constructor_list_or_record_decl constructors_or_record
-| record_binder_body field_body
-| class_rawexpr class
-| smart_global reference
+| constr one_term (* many, many, many *)
+| class_rawexpr class  (* OCaml reserved word *)
+| smart_global reference (* many, many *)
 (*
 | searchabout_query search_item
 *)
-| option_table setting_name
-| argument_spec_block arg_specs
-| more_implicits_block implicits_alt
-| arguments_modifier args_modifier
-| constr_as_binder_kind binder_interp
-| syntax_extension_type explicit_subentry
-| numnotoption numeral_modifier
-| tactic_arg_compat tactic_arg
-| lconstr_pattern cpattern
-| Pltac.tactic ltac_expr
-| sexpr ltac2_scope
-| tac2type5 ltac2_type
-| tac2type2 ltac2_type2
-| tac2type1 ltac2_type1
-| tac2type0 ltac2_type0
-| typ_param ltac2_typevar
-| tac2expr6 ltac2_expr
-| tac2expr5 ltac2_expr5
-| tac2expr3 ltac2_expr3
-| tac2expr2 ltac2_expr2
-| tac2expr1 ltac2_expr1
-| tac2expr0 ltac2_expr0
-| gmatch_list goal_match_list
+| Pltac.tactic ltac_expr  (* many uses in EXTENDs *)
+| ltac2_type5 ltac2_type
+| ltac2_expr6 ltac2_expr
 | starredidentref starred_ident_ref
 ]
 
 simple_tactic: [
-(* due to renaming of tactic_arg; Use LIST1 for function application *)
+(* due to renaming of tactic_value; Use LIST1 for function application *)
 | qualid LIST1 tactic_arg
 ]
 
@@ -2585,7 +2518,7 @@ SPLICE: [
 | ltac_defined_tactics
 | tactic_notation_tactics
 ]
-(* todo: ssrreflect*.rst ref to fix_body is incorrect *)
+(* todo: ssrreflect*.rst ref to fix_decl is incorrect *)
 
 REACHABLE: [
 | command
@@ -2624,17 +2557,7 @@ NOTINRSTS: [
 | q_constr_matching
 | q_goal_matching
 
-(* todo: figure these out
-(*Warning: editedGrammar: Undefined symbol 'ltac1_expr' *)
-| dangling_pattern_extension_rule
-| vernac_aux
-| subprf
-| tactic_mode
-| tac2expr_in_env (* no refs *)
-| tac2mode (* no refs *)
-| ltac_use_default (* from tac2mode *)
-| tacticals
-*)
+
 ]
 
 REACHABLE: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index d3148b5e3a..c764cb6f37 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -17,7 +17,7 @@ constr_pattern: [
 | constr
 ]
 
-lconstr_pattern: [
+cpattern: [
 | lconstr
 ]
 
@@ -58,67 +58,67 @@ universe: [
 ]
 
 lconstr: [
-| operconstr200
+| term200
 ]
 
 constr: [
-| operconstr8
-| "@" global univ_instance
+| term8
+| "@" global univ_annot
 ]
 
-operconstr200: [
+term200: [
 | binder_constr
-| operconstr100
+| term100
 ]
 
-operconstr100: [
-| operconstr99 "<:" operconstr200
-| operconstr99 "<<:" operconstr200
-| operconstr99 ":" operconstr200
-| operconstr99 ":>"
-| operconstr99
+term100: [
+| term99 "<:" term200
+| term99 "<<:" term200
+| term99 ":" term200
+| term99 ":>"
+| term99
 ]
 
-operconstr99: [
-| operconstr90
+term99: [
+| term90
 ]
 
-operconstr90: [
-| operconstr10
+term90: [
+| term10
 ]
 
-operconstr10: [
-| operconstr9 LIST1 appl_arg
-| "@" global univ_instance LIST0 operconstr9
+term10: [
+| term9 LIST1 arg
+| "@" global univ_annot LIST0 term9
 | "@" pattern_ident LIST1 identref
-| operconstr9
+| term9
 ]
 
-operconstr9: [
-| ".." operconstr0 ".."
-| operconstr8
+term9: [
+| ".." term0 ".."
+| term8
 ]
 
-operconstr8: [
-| operconstr1
+term8: [
+| term1
 ]
 
-operconstr1: [
-| operconstr0 ".(" global LIST0 appl_arg ")"
-| operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
-| operconstr0 "%" IDENT
-| operconstr0
+term1: [
+| term0 ".(" global LIST0 arg ")"
+| term0 ".(" "@" global LIST0 ( term9 ) ")"
+| term0 "%" IDENT
+| term0
 ]
 
-operconstr0: [
+term0: [
 | atomic_constr
-| match_constr
-| "(" operconstr200 ")"
+| term_match
+| "(" term200 ")"
 | "{|" record_declaration bar_cbrace
 | "{" binder_constr "}"
-| "`{" operconstr200 "}"
-| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_instance
-| "`(" operconstr200 ")"
+| "`{" term200 "}"
+| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot
+| "`(" term200 ")"
 ]
 
 array_elems: [
@@ -140,27 +140,27 @@ field_def: [
 ]
 
 binder_constr: [
-| "forall" open_binders "," operconstr200
-| "fun" open_binders "=>" operconstr200
-| "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
-| "let" "fix" fix_decl "in" operconstr200
-| "let" "cofix" cofix_decl "in" operconstr200
-| "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200
-| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
-| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
-| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
-| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200
+| "forall" open_binders "," term200
+| "fun" open_binders "=>" term200
+| "let" name binders let_type_cstr ":=" term200 "in" term200
+| "let" "fix" fix_decl "in" term200
+| "let" "cofix" cofix_body "in" term200
+| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
+| "let" "'" pattern200 ":=" term200 "in" term200
+| "let" "'" pattern200 ":=" term200 case_type "in" term200
+| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
+| "if" term200 as_return_type "then" term200 "else" term200
 | "fix" fix_decls
 | "cofix" cofix_decls
 ]
 
-appl_arg: [
+arg: [
 | test_lpar_id_coloneq "(" identref ":=" lconstr ")"
-| operconstr9
+| term9
 ]
 
 atomic_constr: [
-| global univ_instance
+| global univ_annot
 | sort
 | NUMBER
 | string
@@ -179,7 +179,7 @@ evar_instance: [
 |
 ]
 
-univ_instance: [
+univ_annot: [
 | "@{" LIST0 universe_level "}"
 |
 ]
@@ -198,31 +198,31 @@ fix_decls: [
 ]
 
 cofix_decls: [
-| cofix_decl
-| cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref
+| cofix_body
+| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref
 ]
 
 fix_decl: [
-| identref binders_fixannot type_cstr ":=" operconstr200
+| identref binders_fixannot type_cstr ":=" term200
 ]
 
-cofix_decl: [
-| identref binders type_cstr ":=" operconstr200
+cofix_body: [
+| identref binders type_cstr ":=" term200
 ]
 
-match_constr: [
+term_match: [
 | "match" LIST1 case_item SEP "," OPT case_type "with" branches "end"
 ]
 
 case_item: [
-| operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
+| term100 OPT [ "as" name ] OPT [ "in" pattern200 ]
 ]
 
 case_type: [
-| "return" operconstr100
+| "return" term100
 ]
 
-return_type: [
+as_return_type: [
 | OPT [ OPT [ "as" name ] case_type ]
 ]
 
@@ -253,7 +253,7 @@ pattern200: [
 ]
 
 pattern100: [
-| pattern99 ":" operconstr200
+| pattern99 ":" term200
 | pattern99
 ]
 
@@ -335,10 +335,10 @@ closed_binder: [
 ]
 
 typeclass_constraint: [
-| "!" operconstr200
-| "{" name "}" ":" [ "!" | ] operconstr200
-| test_name_colon name ":" [ "!" | ] operconstr200
-| operconstr200
+| "!" term200
+| "{" name "}" ":" [ "!" | ] term200
+| test_name_colon name ":" [ "!" | ] term200
+| term200
 ]
 
 type_cstr: [
@@ -506,7 +506,7 @@ command: [
 | "Remove" "Hints" LIST1 global opt_hintbases
 | "Hint" hint opt_hintbases
 | "Comments" LIST0 comment
-| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info
+| "Declare" "Instance" ident_decl binders ":" term200 hint_info
 | "Declare" "Scope" IDENT
 | "Pwd"
 | "Cd"
@@ -525,13 +525,13 @@ command: [
 | "Print" "Namespace" dirpath
 | "Inspect" natural
 | "Add" "ML" "Path" ne_string
-| "Set" option_table option_setting
-| "Unset" option_table
-| "Print" "Table" option_table
+| "Set" setting_name option_setting
+| "Unset" setting_name
+| "Print" "Table" setting_name
 | "Add" IDENT IDENT LIST1 table_value
 | "Add" IDENT LIST1 table_value
-| "Test" option_table "for" LIST1 table_value
-| "Test" option_table
+| "Test" setting_name "for" LIST1 table_value
+| "Test" setting_name
 | "Remove" IDENT IDENT LIST1 table_value
 | "Remove" IDENT LIST1 table_value
 | "Write" "State" IDENT
@@ -569,7 +569,7 @@ command: [
 | "Show" "Extraction"      (* extraction plugin *)
 | "Set" "Firstorder" "Solver" tactic
 | "Print" "Firstorder" "Solver"
-| "Function" LIST1 function_rec_definition_loc SEP "with"      (* funind plugin *)
+| "Function" LIST1 function_fix_definition SEP "with"      (* funind plugin *)
 | "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
 | "Functional" "Case" fun_scheme_arg      (* funind plugin *)
 | "Generate" "graph" "for" reference      (* funind plugin *)
@@ -686,11 +686,11 @@ command: [
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" constr OPT field_mods      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
-| "Number" "Notation" reference reference reference ":" ident numnotoption
-| "Numeral" "Notation" reference reference reference ":" ident numnotoption
+| "Number" "Notation" reference reference reference ":" ident numeral_modifier
+| "Numeral" "Notation" reference reference reference ":" ident numeral_modifier
 | "String" "Notation" reference reference reference ":" ident
 | "Ltac2" ltac2_entry      (* Ltac2 plugin *)
-| "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
+| "Ltac2" "Eval" ltac2_expr6      (* Ltac2 plugin *)
 | "Print" "Ltac2" reference      (* Ltac2 plugin *)
 ]
 
@@ -745,10 +745,10 @@ attribute_list: [
 ]
 
 attribute: [
-| ident attribute_value
+| ident attr_value
 ]
 
-attribute_value: [
+attr_value: [
 | "=" string
 | "(" attribute_list ")"
 |
@@ -795,10 +795,10 @@ gallina: [
 | def_token ident_decl def_body
 | "Let" ident_decl def_body
 | finite_token LIST1 inductive_definition SEP "with"
-| "Fixpoint" LIST1 rec_definition SEP "with"
-| "Let" "Fixpoint" LIST1 rec_definition SEP "with"
-| "CoFixpoint" LIST1 corec_definition SEP "with"
-| "Let" "CoFixpoint" LIST1 corec_definition SEP "with"
+| "Fixpoint" LIST1 fix_definition SEP "with"
+| "Let" "Fixpoint" LIST1 fix_definition SEP "with"
+| "CoFixpoint" LIST1 cofix_definition SEP "with"
+| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with"
 | "Scheme" LIST1 scheme SEP "with"
 | "Combined" "Scheme" identref "from" LIST1 identref SEP ","
 | "Register" global "as" qualid
@@ -897,7 +897,7 @@ decl_notations: [
 ]
 
 opt_constructors_or_fields: [
-| ":=" constructor_list_or_record_decl
+| ":=" constructors_or_record
 |
 ]
 
@@ -905,7 +905,7 @@ inductive_definition: [
 | opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
 ]
 
-constructor_list_or_record_decl: [
+constructors_or_record: [
 | "|" LIST1 constructor SEP "|"
 | identref constructor_type "|" LIST1 constructor SEP "|"
 | identref constructor_type
@@ -919,11 +919,11 @@ opt_coercion: [
 |
 ]
 
-rec_definition: [
+fix_definition: [
 | ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
 
-corec_definition: [
+cofix_definition: [
 | ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
 
@@ -950,39 +950,39 @@ record_fields: [
 |
 ]
 
-record_binder_body: [
-| binders of_type_with_opt_coercion lconstr
-| binders of_type_with_opt_coercion lconstr ":=" lconstr
+field_body: [
+| binders of_type lconstr
+| binders of_type lconstr ":=" lconstr
 | binders ":=" lconstr
 ]
 
 record_binder: [
 | name
-| name record_binder_body
+| name field_body
 ]
 
 assum_list: [
 | LIST1 assum_coe
-| simple_assum_coe
+| assumpt
 ]
 
 assum_coe: [
-| "(" simple_assum_coe ")"
+| "(" assumpt ")"
 ]
 
-simple_assum_coe: [
-| LIST1 ident_decl of_type_with_opt_coercion lconstr
+assumpt: [
+| LIST1 ident_decl of_type lconstr
 ]
 
 constructor_type: [
-| binders [ of_type_with_opt_coercion lconstr | ]
+| binders [ of_type lconstr | ]
 ]
 
 constructor: [
 | identref constructor_type
 ]
 
-of_type_with_opt_coercion: [
+of_type: [
 | ":>"
 | ":" ">"
 | ":"
@@ -1011,16 +1011,16 @@ gallina_ext: [
 | "Coercion" global ":" class_rawexpr ">->" class_rawexpr
 | "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
 | "Context" LIST1 binder
-| "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
+| "Instance" instance_name ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
 | "Existing" "Instance" global hint_info
 | "Existing" "Instances" LIST1 global OPT [ "|" natural ]
 | "Existing" "Class" global
-| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ]
 | "Implicit" "Type" reserv_list
 | "Implicit" "Types" reserv_list
 | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ]
-| "Export" "Set" option_table option_setting
-| "Export" "Unset" option_table
+| "Export" "Set" setting_name option_setting
+| "Export" "Unset" setting_name
 ]
 
 filtered_import: [
@@ -1142,7 +1142,7 @@ ssexpr0: [
 | "(" ssexpr35 ")" "*"
 ]
 
-arguments_modifier: [
+args_modifier: [
 | "simpl" "nomatch"
 | "simpl" "never"
 | "default" "implicits"
@@ -1164,7 +1164,7 @@ argument_spec: [
 | OPT "!" name OPT scope_delimiter
 ]
 
-argument_spec_block: [
+arg_specs: [
 | argument_spec
 | "/"
 | "&"
@@ -1173,7 +1173,7 @@ argument_spec_block: [
 | "{" LIST1 argument_spec "}" OPT scope_delimiter
 ]
 
-more_implicits_block: [
+implicits_alt: [
 | name
 | "[" LIST1 name "]"
 | "{" LIST1 name "}"
@@ -1282,7 +1282,7 @@ table_value: [
 | STRING
 ]
 
-option_table: [
+setting_name: [
 | LIST1 IDENT
 ]
 
@@ -1391,9 +1391,9 @@ syntax_modifier: [
 | "only" "parsing"
 | "format" STRING OPT STRING
 | IDENT; "," LIST1 IDENT SEP "," "at" level
-| IDENT; "at" level OPT constr_as_binder_kind
-| IDENT constr_as_binder_kind
-| IDENT syntax_extension_type
+| IDENT; "at" level OPT binder_interp
+| IDENT binder_interp
+| IDENT explicit_subentry
 ]
 
 syntax_modifiers: [
@@ -1401,19 +1401,19 @@ syntax_modifiers: [
 |
 ]
 
-syntax_extension_type: [
+explicit_subentry: [
 | "ident"
 | "global"
 | "bigint"
 | "binder"
 | "constr"
-| "constr" at_level_opt OPT constr_as_binder_kind
+| "constr" at_level_opt OPT binder_interp
 | "pattern"
 | "pattern" "at" "level" natural
 | "strict" "pattern"
 | "strict" "pattern" "at" "level" natural
 | "closed" "binder"
-| "custom" IDENT at_level_opt OPT constr_as_binder_kind
+| "custom" IDENT at_level_opt OPT binder_interp
 ]
 
 at_level_opt: [
@@ -1421,7 +1421,7 @@ at_level_opt: [
 |
 ]
 
-constr_as_binder_kind: [
+binder_interp: [
 | "as" "ident"
 | "as" "pattern"
 | "as" "strict" "pattern"
@@ -1789,8 +1789,8 @@ auto_using': [
 |      (* funind plugin *)
 ]
 
-function_rec_definition_loc: [
-| Vernac.rec_definition      (* funind plugin *)
+function_fix_definition: [
+| Vernac.fix_definition      (* funind plugin *)
 ]
 
 fun_scheme_arg: [
@@ -1923,16 +1923,16 @@ eauto_search_strategy: [
 ]
 
 tactic_then_last: [
-| "|" LIST0 ( OPT tactic_expr5 ) SEP "|"
+| "|" LIST0 ( OPT ltac_expr5 ) SEP "|"
 |
 ]
 
-tactic_then_gen: [
-| tactic_expr5 "|" tactic_then_gen
-| tactic_expr5 ".." tactic_then_last
+for_each_goal: [
+| ltac_expr5 "|" for_each_goal
+| ltac_expr5 ".." tactic_then_last
 | ".." tactic_then_last
-| tactic_expr5
-| "|" tactic_then_gen
+| ltac_expr5
+| "|" for_each_goal
 |
 ]
 
@@ -1940,60 +1940,60 @@ tactic_then_locality: [
 | "[" OPT ">"
 ]
 
-tactic_expr5: [
+ltac_expr5: [
 | binder_tactic
-| tactic_expr4
-]
-
-tactic_expr4: [
-| tactic_expr3 ";" binder_tactic
-| tactic_expr3 ";" tactic_expr3
-| tactic_expr3 ";" tactic_then_locality tactic_then_gen "]"
-| tactic_expr3
-]
-
-tactic_expr3: [
-| "try" tactic_expr3
-| "do" int_or_var tactic_expr3
-| "timeout" int_or_var tactic_expr3
-| "time" OPT string tactic_expr3
-| "repeat" tactic_expr3
-| "progress" tactic_expr3
-| "once" tactic_expr3
-| "exactly_once" tactic_expr3
-| "infoH" tactic_expr3
-| "abstract" tactic_expr2
-| "abstract" tactic_expr2 "using" ident
-| selector tactic_expr3
-| tactic_expr2
-]
-
-tactic_expr2: [
-| tactic_expr1 "+" binder_tactic
-| tactic_expr1 "+" tactic_expr2
-| "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2
-| tactic_expr1 "||" binder_tactic
-| tactic_expr1 "||" tactic_expr2
-| tactic_expr1
-]
-
-tactic_expr1: [
+| ltac_expr4
+]
+
+ltac_expr4: [
+| ltac_expr3 ";" binder_tactic
+| ltac_expr3 ";" ltac_expr3
+| ltac_expr3 ";" tactic_then_locality for_each_goal "]"
+| ltac_expr3
+]
+
+ltac_expr3: [
+| "try" ltac_expr3
+| "do" int_or_var ltac_expr3
+| "timeout" int_or_var ltac_expr3
+| "time" OPT string ltac_expr3
+| "repeat" ltac_expr3
+| "progress" ltac_expr3
+| "once" ltac_expr3
+| "exactly_once" ltac_expr3
+| "infoH" ltac_expr3
+| "abstract" ltac_expr2
+| "abstract" ltac_expr2 "using" ident
+| "only" selector ":" ltac_expr3
+| ltac_expr2
+]
+
+ltac_expr2: [
+| ltac_expr1 "+" binder_tactic
+| ltac_expr1 "+" ltac_expr2
+| "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2
+| ltac_expr1 "||" binder_tactic
+| ltac_expr1 "||" ltac_expr2
+| ltac_expr1
+]
+
+ltac_expr1: [
 | match_key "goal" "with" match_context_list "end"
 | match_key "reverse" "goal" "with" match_context_list "end"
-| match_key tactic_expr5 "with" match_list "end"
-| "first" "[" LIST0 tactic_expr5 SEP "|" "]"
-| "solve" "[" LIST0 tactic_expr5 SEP "|" "]"
+| match_key ltac_expr5 "with" match_list "end"
+| "first" "[" LIST0 ltac_expr5 SEP "|" "]"
+| "solve" "[" LIST0 ltac_expr5 SEP "|" "]"
 | "idtac" LIST0 message_token
 | failkw [ int_or_var | ] LIST0 message_token
 | simple_tactic
-| tactic_arg
-| reference LIST0 tactic_arg_compat
-| tactic_expr0
+| tactic_value
+| reference LIST0 tactic_arg
+| ltac_expr0
 ]
 
-tactic_expr0: [
-| "(" tactic_expr5 ")"
-| "[" ">" tactic_then_gen "]"
+ltac_expr0: [
+| "(" ltac_expr5 ")"
+| "[" ">" for_each_goal "]"
 | tactic_atom
 ]
 
@@ -2003,17 +2003,17 @@ failkw: [
 ]
 
 binder_tactic: [
-| "fun" LIST1 input_fun "=>" tactic_expr5
-| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
+| "fun" LIST1 input_fun "=>" ltac_expr5
+| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
 ]
 
-tactic_arg_compat: [
-| tactic_arg
+tactic_arg: [
+| tactic_value
 | Constr.constr
 | "()"
 ]
 
-tactic_arg: [
+tactic_value: [
 | constr_eval
 | "fresh" LIST0 fresh_id
 | "type_term" uconstr
@@ -2054,26 +2054,26 @@ input_fun: [
 ]
 
 let_clause: [
-| identref ":=" tactic_expr5
-| "_" ":=" tactic_expr5
-| identref LIST1 input_fun ":=" tactic_expr5
+| identref ":=" ltac_expr5
+| "_" ":=" ltac_expr5
+| identref LIST1 input_fun ":=" ltac_expr5
 ]
 
 match_pattern: [
-| "context" OPT Constr.ident "[" Constr.lconstr_pattern "]"
-| Constr.lconstr_pattern
+| "context" OPT Constr.ident "[" Constr.cpattern "]"
+| Constr.cpattern
 ]
 
-match_hyps: [
+match_hyp: [
 | name ":" match_pattern
 | name ":=" "[" match_pattern "]" ":" match_pattern
 | name ":=" match_pattern
 ]
 
 match_context_rule: [
-| LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5
-| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5
-| "_" "=>" tactic_expr5
+| LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr5
+| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr5
+| "_" "=>" ltac_expr5
 ]
 
 match_context_list: [
@@ -2082,8 +2082,8 @@ match_context_list: [
 ]
 
 match_rule: [
-| match_pattern "=>" tactic_expr5
-| "_" "=>" tactic_expr5
+| match_pattern "=>" ltac_expr5
+| "_" "=>" ltac_expr5
 ]
 
 match_list: [
@@ -2103,12 +2103,12 @@ ltac_def_kind: [
 ]
 
 tacdef_body: [
-| Constr.global LIST1 input_fun ltac_def_kind tactic_expr5
-| Constr.global ltac_def_kind tactic_expr5
+| Constr.global LIST1 input_fun ltac_def_kind ltac_expr5
+| Constr.global ltac_def_kind ltac_expr5
 ]
 
 tactic: [
-| tactic_expr5
+| ltac_expr5
 ]
 
 range_selector: [
@@ -2121,17 +2121,13 @@ range_selector_or_nth: [
 | natural OPT [ "," LIST1 range_selector SEP "," ]
 ]
 
-selector_body: [
+selector: [
 | range_selector_or_nth
 | test_bracket_ident "[" ident "]"
 ]
 
-selector: [
-| "only" selector_body ":"
-]
-
 toplevel_selector: [
-| selector_body ":"
+| selector ":"
 | "!" ":"
 | "all" ":"
 ]
@@ -2147,8 +2143,8 @@ G_LTAC_hint: [
 | "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
 ]
 
-G_LTAC_operconstr0: [
-| "ltac" ":" "(" Pltac.tactic_expr ")"
+G_LTAC_term0: [
+| "ltac" ":" "(" Pltac.ltac_expr ")"
 ]
 
 ltac_selector: [
@@ -2327,7 +2323,7 @@ intropattern: [
 ]
 
 simple_intropattern: [
-| simple_intropattern_closed LIST0 [ "%" operconstr0 ]
+| simple_intropattern_closed LIST0 [ "%" term0 ]
 ]
 
 simple_intropattern_closed: [
@@ -2356,7 +2352,7 @@ with_bindings: [
 |
 ]
 
-red_flags: [
+red_flag: [
 | "beta"
 | "iota"
 | "match"
@@ -2373,7 +2369,7 @@ delta_flag: [
 ]
 
 strategy_flag: [
-| LIST1 red_flags
+| LIST1 red_flag
 | delta_flag
 ]
 
@@ -2500,7 +2496,7 @@ as_name: [
 ]
 
 by_tactic: [
-| "by" tactic_expr3
+| "by" ltac_expr3
 |
 ]
 
@@ -2553,7 +2549,7 @@ field_mods: [
 | "(" LIST1 field_mod SEP "," ")"      (* ring plugin *)
 ]
 
-numnotoption: [
+numeral_modifier: [
 |
 | "(" "warning" "after" bignat ")"
 | "(" "abstract" "after" bignat ")"
@@ -2576,50 +2572,50 @@ tac2pat0: [
 
 atomic_tac2pat: [
 |      (* Ltac2 plugin *)
-| tac2pat1 ":" tac2type5      (* Ltac2 plugin *)
+| tac2pat1 ":" ltac2_type5      (* Ltac2 plugin *)
 | tac2pat1 "," LIST0 tac2pat1 SEP ","      (* Ltac2 plugin *)
 | tac2pat1      (* Ltac2 plugin *)
 ]
 
-tac2expr6: [
-| tac2expr5 ";" tac2expr6      (* Ltac2 plugin *)
-| tac2expr5      (* Ltac2 plugin *)
+ltac2_expr6: [
+| ltac2_expr5 ";" ltac2_expr6      (* Ltac2 plugin *)
+| ltac2_expr5      (* Ltac2 plugin *)
 ]
 
-tac2expr5: [
-| "fun" LIST1 G_LTAC2_input_fun "=>" tac2expr6      (* Ltac2 plugin *)
-| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" tac2expr6      (* Ltac2 plugin *)
-| "match" tac2expr5 "with" G_LTAC2_branches "end"      (* Ltac2 plugin *)
-| tac2expr4      (* Ltac2 plugin *)
+ltac2_expr5: [
+| "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6      (* Ltac2 plugin *)
+| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6      (* Ltac2 plugin *)
+| "match" ltac2_expr5 "with" G_LTAC2_branches "end"      (* Ltac2 plugin *)
+| ltac2_expr4      (* Ltac2 plugin *)
 ]
 
-tac2expr4: [
-| tac2expr3      (* Ltac2 plugin *)
+ltac2_expr4: [
+| ltac2_expr3      (* Ltac2 plugin *)
 ]
 
-tac2expr3: [
-| tac2expr2 "," LIST1 tac2expr2 SEP ","      (* Ltac2 plugin *)
-| tac2expr2      (* Ltac2 plugin *)
+ltac2_expr3: [
+| ltac2_expr2 "," LIST1 ltac2_expr2 SEP ","      (* Ltac2 plugin *)
+| ltac2_expr2      (* Ltac2 plugin *)
 ]
 
-tac2expr2: [
-| tac2expr1 "::" tac2expr2      (* Ltac2 plugin *)
-| tac2expr1      (* Ltac2 plugin *)
+ltac2_expr2: [
+| ltac2_expr1 "::" ltac2_expr2      (* Ltac2 plugin *)
+| ltac2_expr1      (* Ltac2 plugin *)
 ]
 
-tac2expr1: [
-| tac2expr0 LIST1 tac2expr0      (* Ltac2 plugin *)
-| tac2expr0 ".(" Prim.qualid ")"      (* Ltac2 plugin *)
-| tac2expr0 ".(" Prim.qualid ")" ":=" tac2expr5      (* Ltac2 plugin *)
-| tac2expr0      (* Ltac2 plugin *)
+ltac2_expr1: [
+| ltac2_expr0 LIST1 ltac2_expr0      (* Ltac2 plugin *)
+| ltac2_expr0 ".(" Prim.qualid ")"      (* Ltac2 plugin *)
+| ltac2_expr0 ".(" Prim.qualid ")" ":=" ltac2_expr5      (* Ltac2 plugin *)
+| ltac2_expr0      (* Ltac2 plugin *)
 ]
 
-tac2expr0: [
-| "(" tac2expr6 ")"      (* Ltac2 plugin *)
-| "(" tac2expr6 ":" tac2type5 ")"      (* Ltac2 plugin *)
+ltac2_expr0: [
+| "(" ltac2_expr6 ")"      (* Ltac2 plugin *)
+| "(" ltac2_expr6 ":" ltac2_type5 ")"      (* Ltac2 plugin *)
 | "()"      (* Ltac2 plugin *)
 | "(" ")"      (* Ltac2 plugin *)
-| "[" LIST0 tac2expr5 SEP ";" "]"      (* Ltac2 plugin *)
+| "[" LIST0 ltac2_expr5 SEP ";" "]"      (* Ltac2 plugin *)
 | "{" tac2rec_fieldexprs "}"      (* Ltac2 plugin *)
 | G_LTAC2_tactic_atom      (* Ltac2 plugin *)
 ]
@@ -2631,7 +2627,7 @@ G_LTAC2_branches: [
 ]
 
 branch: [
-| tac2pat1 "=>" tac2expr6      (* Ltac2 plugin *)
+| tac2pat1 "=>" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 rec_flag: [
@@ -2644,7 +2640,7 @@ mut_flag: [
 |      (* Ltac2 plugin *)
 ]
 
-typ_param: [
+ltac2_typevar: [
 | "'" Prim.ident      (* Ltac2 plugin *)
 ]
 
@@ -2658,48 +2654,48 @@ G_LTAC2_tactic_atom: [
 | "constr" ":" "(" Constr.lconstr ")"      (* Ltac2 plugin *)
 | "open_constr" ":" "(" Constr.lconstr ")"      (* Ltac2 plugin *)
 | "ident" ":" "(" lident ")"      (* Ltac2 plugin *)
-| "pattern" ":" "(" Constr.lconstr_pattern ")"      (* Ltac2 plugin *)
+| "pattern" ":" "(" Constr.cpattern ")"      (* Ltac2 plugin *)
 | "reference" ":" "(" globref ")"      (* Ltac2 plugin *)
 | "ltac1" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
 | "ltac1val" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
 ]
 
 ltac1_expr_in_env: [
-| test_ltac1_env LIST0 locident "|-" ltac1_expr      (* Ltac2 plugin *)
-| ltac1_expr      (* Ltac2 plugin *)
+| test_ltac1_env LIST0 locident "|-" ltac_expr5      (* Ltac2 plugin *)
+| ltac_expr5      (* Ltac2 plugin *)
 ]
 
 tac2expr_in_env: [
-| test_ltac1_env LIST0 locident "|-" tac2expr6      (* Ltac2 plugin *)
-| tac2expr6      (* Ltac2 plugin *)
+| test_ltac1_env LIST0 locident "|-" ltac2_expr6      (* Ltac2 plugin *)
+| ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 G_LTAC2_let_clause: [
-| let_binder ":=" tac2expr6      (* Ltac2 plugin *)
+| let_binder ":=" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 let_binder: [
 | LIST1 G_LTAC2_input_fun      (* Ltac2 plugin *)
 ]
 
-tac2type5: [
-| tac2type2 "->" tac2type5      (* Ltac2 plugin *)
-| tac2type2      (* Ltac2 plugin *)
+ltac2_type5: [
+| ltac2_type2 "->" ltac2_type5      (* Ltac2 plugin *)
+| ltac2_type2      (* Ltac2 plugin *)
 ]
 
-tac2type2: [
-| tac2type1 "*" LIST1 tac2type1 SEP "*"      (* Ltac2 plugin *)
-| tac2type1      (* Ltac2 plugin *)
+ltac2_type2: [
+| ltac2_type1 "*" LIST1 ltac2_type1 SEP "*"      (* Ltac2 plugin *)
+| ltac2_type1      (* Ltac2 plugin *)
 ]
 
-tac2type1: [
-| tac2type0 Prim.qualid      (* Ltac2 plugin *)
-| tac2type0      (* Ltac2 plugin *)
+ltac2_type1: [
+| ltac2_type0 Prim.qualid      (* Ltac2 plugin *)
+| ltac2_type0      (* Ltac2 plugin *)
 ]
 
-tac2type0: [
-| "(" LIST1 tac2type5 SEP "," ")" OPT Prim.qualid      (* Ltac2 plugin *)
-| typ_param      (* Ltac2 plugin *)
+ltac2_type0: [
+| "(" LIST1 ltac2_type5 SEP "," ")" OPT Prim.qualid      (* Ltac2 plugin *)
+| ltac2_typevar      (* Ltac2 plugin *)
 | "_"      (* Ltac2 plugin *)
 | Prim.qualid      (* Ltac2 plugin *)
 ]
@@ -2718,7 +2714,7 @@ G_LTAC2_input_fun: [
 ]
 
 tac2def_body: [
-| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" tac2expr6      (* Ltac2 plugin *)
+| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 tac2def_val: [
@@ -2726,11 +2722,11 @@ tac2def_val: [
 ]
 
 tac2def_mut: [
-| "Set" Prim.qualid OPT [ "as" locident ] ":=" tac2expr6      (* Ltac2 plugin *)
+| "Set" Prim.qualid OPT [ "as" locident ] ":=" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 tac2typ_knd: [
-| tac2type5      (* Ltac2 plugin *)
+| ltac2_type5      (* Ltac2 plugin *)
 | "[" ".." "]"      (* Ltac2 plugin *)
 | "[" tac2alg_constructors "]"      (* Ltac2 plugin *)
 | "{" tac2rec_fields "}"      (* Ltac2 plugin *)
@@ -2743,7 +2739,7 @@ tac2alg_constructors: [
 
 tac2alg_constructor: [
 | Prim.ident      (* Ltac2 plugin *)
-| Prim.ident "(" LIST0 tac2type5 SEP "," ")"      (* Ltac2 plugin *)
+| Prim.ident "(" LIST0 ltac2_type5 SEP "," ")"      (* Ltac2 plugin *)
 ]
 
 tac2rec_fields: [
@@ -2754,7 +2750,7 @@ tac2rec_fields: [
 ]
 
 tac2rec_field: [
-| mut_flag Prim.ident ":" tac2type5      (* Ltac2 plugin *)
+| mut_flag Prim.ident ":" ltac2_type5      (* Ltac2 plugin *)
 ]
 
 tac2rec_fieldexprs: [
@@ -2765,13 +2761,13 @@ tac2rec_fieldexprs: [
 ]
 
 tac2rec_fieldexpr: [
-| Prim.qualid ":=" tac2expr1      (* Ltac2 plugin *)
+| Prim.qualid ":=" ltac2_expr1      (* Ltac2 plugin *)
 ]
 
 tac2typ_prm: [
 |      (* Ltac2 plugin *)
-| typ_param      (* Ltac2 plugin *)
-| "(" LIST1 typ_param SEP "," ")"      (* Ltac2 plugin *)
+| ltac2_typevar      (* Ltac2 plugin *)
+| "(" LIST1 ltac2_typevar SEP "," ")"      (* Ltac2 plugin *)
 ]
 
 tac2typ_def: [
@@ -2789,7 +2785,7 @@ tac2def_typ: [
 ]
 
 tac2def_ext: [
-| "@" "external" locident ":" tac2type5 ":=" Prim.string Prim.string      (* Ltac2 plugin *)
+| "@" "external" locident ":" ltac2_type5 ":=" Prim.string Prim.string      (* Ltac2 plugin *)
 ]
 
 syn_node: [
@@ -2797,11 +2793,11 @@ syn_node: [
 | Prim.ident      (* Ltac2 plugin *)
 ]
 
-sexpr: [
+ltac2_scope: [
 | Prim.string      (* Ltac2 plugin *)
 | Prim.integer      (* Ltac2 plugin *)
 | syn_node      (* Ltac2 plugin *)
-| syn_node "(" LIST1 sexpr SEP "," ")"      (* Ltac2 plugin *)
+| syn_node "(" LIST1 ltac2_scope SEP "," ")"      (* Ltac2 plugin *)
 ]
 
 syn_level: [
@@ -2810,7 +2806,7 @@ syn_level: [
 ]
 
 tac2def_syn: [
-| "Notation" LIST1 sexpr syn_level ":=" tac2expr6      (* Ltac2 plugin *)
+| "Notation" LIST1 ltac2_scope syn_level ":=" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 lident: [
@@ -3028,28 +3024,28 @@ q_rewriting: [
 ]
 
 G_LTAC2_tactic_then_last: [
-| "|" LIST0 ( OPT tac2expr6 ) SEP "|"      (* Ltac2 plugin *)
+| "|" LIST0 ( OPT ltac2_expr6 ) SEP "|"      (* Ltac2 plugin *)
 |      (* Ltac2 plugin *)
 ]
 
-G_LTAC2_tactic_then_gen: [
-| tac2expr6 "|" G_LTAC2_tactic_then_gen      (* Ltac2 plugin *)
-| tac2expr6 ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
+G_LTAC2_for_each_goal: [
+| ltac2_expr6 "|" G_LTAC2_for_each_goal      (* Ltac2 plugin *)
+| ltac2_expr6 ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
 | ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
-| tac2expr6      (* Ltac2 plugin *)
-| "|" G_LTAC2_tactic_then_gen      (* Ltac2 plugin *)
+| ltac2_expr6      (* Ltac2 plugin *)
+| "|" G_LTAC2_for_each_goal      (* Ltac2 plugin *)
 |      (* Ltac2 plugin *)
 ]
 
 q_dispatch: [
-| G_LTAC2_tactic_then_gen      (* Ltac2 plugin *)
+| G_LTAC2_for_each_goal      (* Ltac2 plugin *)
 ]
 
 q_occurrences: [
 | G_LTAC2_occs      (* Ltac2 plugin *)
 ]
 
-red_flag: [
+ltac2_red_flag: [
 | "beta"      (* Ltac2 plugin *)
 | "iota"      (* Ltac2 plugin *)
 | "match"      (* Ltac2 plugin *)
@@ -3080,7 +3076,7 @@ G_LTAC2_delta_flag: [
 ]
 
 G_LTAC2_strategy_flag: [
-| LIST1 red_flag      (* Ltac2 plugin *)
+| LIST1 ltac2_red_flag      (* Ltac2 plugin *)
 | G_LTAC2_delta_flag      (* Ltac2 plugin *)
 ]
 
@@ -3098,12 +3094,12 @@ q_hintdb: [
 ]
 
 G_LTAC2_match_pattern: [
-| "context" OPT Prim.ident "[" Constr.lconstr_pattern "]"      (* Ltac2 plugin *)
-| Constr.lconstr_pattern      (* Ltac2 plugin *)
+| "context" OPT Prim.ident "[" Constr.cpattern "]"      (* Ltac2 plugin *)
+| Constr.cpattern      (* Ltac2 plugin *)
 ]
 
 G_LTAC2_match_rule: [
-| G_LTAC2_match_pattern "=>" tac2expr6      (* Ltac2 plugin *)
+| G_LTAC2_match_pattern "=>" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 G_LTAC2_match_list: [
@@ -3124,16 +3120,16 @@ gmatch_pattern: [
 ]
 
 gmatch_rule: [
-| gmatch_pattern "=>" tac2expr6      (* Ltac2 plugin *)
+| gmatch_pattern "=>" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
-gmatch_list: [
+goal_match_list: [
 | LIST1 gmatch_rule SEP "|"      (* Ltac2 plugin *)
 | "|" LIST1 gmatch_rule SEP "|"      (* Ltac2 plugin *)
 ]
 
 q_goal_matching: [
-| gmatch_list      (* Ltac2 plugin *)
+| goal_match_list      (* Ltac2 plugin *)
 ]
 
 move_location: [
@@ -3167,7 +3163,7 @@ G_LTAC2_as_ipat: [
 ]
 
 G_LTAC2_by_tactic: [
-| "by" tac2expr6      (* Ltac2 plugin *)
+| "by" ltac2_expr6      (* Ltac2 plugin *)
 |      (* Ltac2 plugin *)
 ]
 
@@ -3190,11 +3186,11 @@ ltac2_entry: [
 ]
 
 ltac2_expr: [
-| tac2expr6      (* Ltac2 plugin *)
+| _ltac2_expr      (* Ltac2 plugin *)
 ]
 
 tac2mode: [
-| ltac2_expr ltac_use_default      (* Ltac2 plugin *)
+| ltac2_expr6 ltac_use_default      (* Ltac2 plugin *)
 | G_vernac.query_command      (* Ltac2 plugin *)
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index ff1efa5375..12a7bc684d 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -320,11 +320,11 @@ univ_constraint: [
 ]
 
 term_fix: [
-| "let" "fix" fix_body "in" term
-| "fix" fix_body OPT ( LIST1 ( "with" fix_body ) "for" ident )
+| "let" "fix" fix_decl "in" term
+| "fix" fix_decl OPT ( LIST1 ( "with" fix_decl ) "for" ident )
 ]
 
-fix_body: [
+fix_decl: [
 | ident LIST0 binder OPT fixannot OPT ( ":" type ) ":=" term
 ]
 
@@ -885,6 +885,7 @@ command: [
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
 | "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
+| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST1 qualid
 | "Typeclasses" "Opaque" LIST1 qualid
@@ -909,7 +910,6 @@ command: [
 | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family
 | "Declare" "Left" "Step" one_term
 | "Declare" "Right" "Step" one_term
-| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
 | "String" "Notation" qualid qualid qualid ":" scope_name
 | "SubClass" ident_decl def_body
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
@@ -1435,7 +1435,7 @@ simple_tactic: [
 | "notypeclasses" "refine" one_term
 | "simple" "notypeclasses" "refine" one_term
 | "solve_constraints"
-| "subst" OPT ( LIST1 ident )
+| "subst" LIST0 ident
 | "simple" "subst"
 | "evar" "(" ident ":" term ")"
 | "evar" one_term