Rename misc nonterminals

5 files changed, 231 insertions, 299 deletions

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/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index fc5aa3f93d..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
@@ -486,7 +486,7 @@ Displaying information about notations
      | "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
        :
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 1e4101db1c..d75b5f6965 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -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
 ]
@@ -191,9 +195,9 @@ goal_tactics: [
 | 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 ltac_expr5 ".." OPT ( "|" goal_tactics )
 ]
@@ -211,9 +215,9 @@ ltac2_goal_tactics: [
 | LIST0 ( OPT tac2expr6 ) 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
 ]
@@ -257,11 +261,6 @@ 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 term100 OPT [ "as" name ] OPT [ "in" pattern200 ]
 | WITH term100 OPT ("as" name) OPT [ "in" pattern200 ]
@@ -272,8 +271,8 @@ binder_constr: [
 | 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_decl "in" term200
+| MOVETO term_fix "let" "fix" fix_body "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
@@ -295,7 +294,7 @@ term_let: [
 ]
 
 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 "_"
@@ -309,8 +308,8 @@ atomic_constr: [
 ]
 
 ltac_expr0: [
-| REPLACE "[" ">" tactic_then_gen "]"
-| WITH "[>" tactic_then_gen "]"
+| REPLACE "[" ">" for_each_goal "]"
+| WITH "[>" for_each_goal "]"
 ]
 
 (* lexer token *)
@@ -354,7 +353,7 @@ term100: [
 ]
 
 constr: [
-| REPLACE "@" global univ_instance
+| REPLACE "@" global univ_annot
 | WITH "@" qualid_annotated
 | MOVETO term_explicit "@" qualid_annotated
 ]
@@ -362,11 +361,11 @@ constr: [
 term10: [
 (* Separate this LIST0 in the nonempty and the empty case *)
 (* The empty case is covered by constr *)
-| REPLACE "@" global univ_instance LIST0 term9
+| REPLACE "@" global univ_annot LIST0 term9
 | WITH "@" qualid_annotated LIST1 term9
 | REPLACE term9
 | WITH constr
-| MOVETO term_application term9 LIST1 appl_arg
+| 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
@@ -379,12 +378,12 @@ term9: [
 ]
 
 term1: [
-| REPLACE term0 ".(" global LIST0 appl_arg ")"
-| WITH    term0 ".(" global LIST0 appl_arg ")" (* huh? *)
+| 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 appl_arg ")"
+| MOVETO term_projection term0 ".(" global LIST0 arg ")"
 | MOVETO term_projection term0 ".(" "@" global LIST0 ( term9 ) ")"
 ]
 
@@ -397,20 +396,20 @@ term0: [
 | MOVETO term_generalizing "`{" term200 "}"
 | MOVETO term_generalizing "`(" term200 ")"
 | MOVETO term_ltac "ltac" ":" "(" ltac_expr5 ")"
-| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_instance
-| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_instance
+| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_annot
+| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_annot
 ]
 
 fix_decls: [
-| DELETE fix_decl
-| REPLACE fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
-| WITH fix_decl OPT ( LIST1 ("with" fix_decl) "for" identref )
+| DELETE fix_body
+| REPLACE fix_body "with" LIST1 fix_body SEP "with" "for" identref
+| WITH fix_body OPT ( LIST1 ("with" fix_body) "for" identref )
 ]
 
 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: [
@@ -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,10 +718,10 @@ 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 "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 ]
 
@@ -832,20 +823,20 @@ ltac_expr5: [
 ltac_constructs: [
 (* repeated in main ltac grammar - need to create a COPY edit *)
 | ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
-| ltac_expr3 ";" "[" tactic_then_gen "]"
+| ltac_expr3 ";" "[" for_each_goal "]"
 
 | 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 "]"
+| "[>" for_each_goal "]"
 | toplevel_selector ltac_expr5
 ]
 
 ltac_expr4: [
-| REPLACE ltac_expr3 ";" tactic_then_gen "]"
-| WITH ltac_expr3 ";" "[" tactic_then_gen "]"
+| 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
@@ -885,27 +876,27 @@ ltac_expr1: [
 | 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_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 "=>" ltac_expr5
-| DELETE "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" ltac_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
 ]
@@ -923,7 +914,7 @@ match_rule: [
 | 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
@@ -1106,8 +1097,8 @@ simple_tactic: [
 | DELETE "transparent_abstract" tactic3
 | REPLACE "transparent_abstract" tactic3 "using" ident
 | WITH "transparent_abstract" ltac_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 )
+| "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
@@ -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,7 +1358,7 @@ syntax_extension_type: [
 | DELETE "constr"    (* covered by another prod *)
 ]
 
-numnotoption: [
+numeral_modifier: [
 | OPTINREF
 ]
 
@@ -1377,21 +1368,21 @@ binder_tactic: [
 | 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
 ]
 
@@ -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 ":"
@@ -1943,7 +1934,7 @@ tactic_notation_tactics: [
 ]
 
 (* defined in OCaml outside of mlgs *)
-tactic_arg: [
+tactic_value: [
 | "uconstr" ":" "(" term200 ")"
 | MOVEALLBUT simple_tactic
 ]
@@ -1952,10 +1943,6 @@ nonterminal: [ ]
 
 value_tactic: [ ]
 
-RENAME: [
-| tactic_arg tactic_value
-]
-
 syn_value: [
 | IDENT; ":" "(" nonterminal ")"
 ]
@@ -1975,7 +1962,7 @@ 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 OPT "reverse" "goal" "with" goal_match_list "end"
 ]
 
 simple_tactic: [
@@ -2214,14 +2201,7 @@ tac2expr5: [
 | 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 *)
 ]
 
@@ -2381,7 +2361,6 @@ SPLICE: [
 | decorated_vernac
 | ext_module_expr
 | ext_module_type
-| pattern_ident
 | test
 | binder_constr
 | atomic_constr
@@ -2449,7 +2428,6 @@ SPLICE: [
 | intropatterns
 | instance_name
 | failkw
-| selector
 | ne_in_or_out_modules
 | search_queries
 | locatable
@@ -2489,56 +2467,27 @@ 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
 | ltac_expr5 ltac_expr
 
 (* | nonsimple_intropattern intropattern (* ltac2 *) *)
 
 | 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
+| Pltac.tactic ltac_expr  (* many uses in EXTENDs *)
+| tac2type5 ltac2_type (* careful *)
 | tac2type2 ltac2_type2
 | tac2type1 ltac2_type1
 | tac2type0 ltac2_type0
@@ -2549,12 +2498,11 @@ RENAME: [
 | tac2expr2 ltac2_expr2
 | tac2expr1 ltac2_expr1
 | tac2expr0 ltac2_expr0
-| gmatch_list goal_match_list
 | 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
 ]
 
@@ -2615,17 +2563,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 538ab8947c..a8cade6041 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -17,7 +17,7 @@ constr_pattern: [
 | constr
 ]
 
-lconstr_pattern: [
+cpattern: [
 | lconstr
 ]
 
@@ -63,7 +63,7 @@ lconstr: [
 
 constr: [
 | term8
-| "@" global univ_instance
+| "@" global univ_annot
 ]
 
 term200: [
@@ -88,9 +88,9 @@ term90: [
 ]
 
 term10: [
-| term9 LIST1 appl_arg
-| "@" global univ_instance LIST0 term9
-| "@" pattern_identref LIST1 identref
+| term9 LIST1 arg
+| "@" global univ_annot LIST0 term9
+| "@" pattern_ident LIST1 identref
 | term9
 ]
 
@@ -104,7 +104,7 @@ term8: [
 ]
 
 term1: [
-| term0 ".(" global LIST0 appl_arg ")"
+| term0 ".(" global LIST0 arg ")"
 | term0 ".(" "@" global LIST0 ( term9 ) ")"
 | term0 "%" IDENT
 | term0
@@ -112,12 +112,12 @@ term1: [
 
 term0: [
 | atomic_constr
-| match_constr
+| term_match
 | "(" term200 ")"
 | "{|" record_declaration bar_cbrace
 | "{" binder_constr "}"
 | "`{" term200 "}"
-| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_instance
+| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot
 | "`(" term200 ")"
 ]
 
@@ -143,35 +143,35 @@ binder_constr: [
 | "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_decl "in" term200
-| "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" term200 "in" term200
+| "let" "fix" fix_body "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 return_type "then" term200 "else" term200
+| "if" term200 as_return_type "then" term200 "else" term200
 | "fix" fix_decls
 | "cofix" cofix_decls
 ]
 
-appl_arg: [
-| test_lpar_id_coloneq "(" ident ":=" lconstr ")"
+arg: [
+| test_lpar_id_coloneq "(" identref ":=" lconstr ")"
 | term9
 ]
 
 atomic_constr: [
-| global univ_instance
+| global univ_annot
 | sort
 | NUMBER
 | string
 | "_"
-| "?" "[" ident "]"
+| "?" "[" identref "]"
 | "?" "[" pattern_ident "]"
 | pattern_ident evar_instance
 ]
 
 inst: [
-| ident ":=" lconstr
+| identref ":=" lconstr
 ]
 
 evar_instance: [
@@ -179,7 +179,7 @@ evar_instance: [
 |
 ]
 
-univ_instance: [
+univ_annot: [
 | "@{" LIST0 universe_level "}"
 |
 ]
@@ -193,24 +193,24 @@ universe_level: [
 ]
 
 fix_decls: [
-| fix_decl
-| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
+| fix_body
+| fix_body "with" LIST1 fix_body SEP "with" "for" identref
 ]
 
 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: [
+fix_body: [
 | identref binders_fixannot type_cstr ":=" term200
 ]
 
-cofix_decl: [
+cofix_body: [
 | identref binders type_cstr ":=" term200
 ]
 
-match_constr: [
+term_match: [
 | "match" LIST1 case_item SEP "," OPT case_type "with" branches "end"
 ]
 
@@ -222,7 +222,7 @@ case_type: [
 | "return" term100
 ]
 
-return_type: [
+as_return_type: [
 | OPT [ OPT [ "as" name ] case_type ]
 ]
 
@@ -362,16 +362,12 @@ pattern_ident: [
 | LEFTQMARK ident
 ]
 
-pattern_identref: [
-| pattern_ident
-]
-
-var: [
+identref: [
 | ident
 ]
 
-identref: [
-| ident
+hyp: [
+| identref
 ]
 
 field: [
@@ -529,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
@@ -596,9 +592,9 @@ command: [
 | "Optimize" "Proof"
 | "Optimize" "Heap"
 | "Hint" "Cut" "[" hints_path "]" opthints
-| "Typeclasses" "Transparent" LIST0 reference
-| "Typeclasses" "Opaque" LIST0 reference
-| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT integer
+| "Typeclasses" "Transparent" LIST1 reference
+| "Typeclasses" "Opaque" LIST1 reference
+| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural
 | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ]
 | "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ]
 | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
@@ -615,6 +611,7 @@ command: [
 | "Solve" "Obligation" natural "of" ident "with" tactic
 | "Solve" "Obligation" natural "with" tactic
 | "Solve" "Obligations" "of" ident "with" tactic
+| "Solve" "Obligations" "of" ident
 | "Solve" "Obligations" "with" tactic
 | "Solve" "Obligations"
 | "Solve" "All" "Obligations" "with" tactic
@@ -689,8 +686,8 @@ 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 *)
@@ -748,10 +745,10 @@ attribute_list: [
 ]
 
 attribute: [
-| ident attribute_value
+| ident attr_value
 ]
 
-attribute_value: [
+attr_value: [
 | "=" string
 | "(" attribute_list ")"
 |
@@ -798,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
@@ -900,7 +897,7 @@ decl_notations: [
 ]
 
 opt_constructors_or_fields: [
-| ":=" constructor_list_or_record_decl
+| ":=" constructors_or_record
 |
 ]
 
@@ -908,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
@@ -922,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
 ]
 
@@ -953,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: [
 | ":>"
 | ":" ">"
 | ":"
@@ -1018,12 +1015,12 @@ gallina_ext: [
 | "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: [
@@ -1145,7 +1142,7 @@ ssexpr0: [
 | "(" ssexpr35 ")" "*"
 ]
 
-arguments_modifier: [
+args_modifier: [
 | "simpl" "nomatch"
 | "simpl" "never"
 | "default" "implicits"
@@ -1167,7 +1164,7 @@ argument_spec: [
 | OPT "!" name OPT scope_delimiter
 ]
 
-argument_spec_block: [
+arg_specs: [
 | argument_spec
 | "/"
 | "&"
@@ -1176,7 +1173,7 @@ argument_spec_block: [
 | "{" LIST1 argument_spec "}" OPT scope_delimiter
 ]
 
-more_implicits_block: [
+implicits_alt: [
 | name
 | "[" LIST1 name "]"
 | "{" LIST1 name "}"
@@ -1285,7 +1282,7 @@ table_value: [
 | STRING
 ]
 
-option_table: [
+setting_name: [
 | LIST1 IDENT
 ]
 
@@ -1394,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: [
@@ -1404,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: [
@@ -1424,7 +1421,7 @@ at_level_opt: [
 |
 ]
 
-constr_as_binder_kind: [
+binder_interp: [
 | "as" "ident"
 | "as" "pattern"
 | "as" "strict" "pattern"
@@ -1551,7 +1548,7 @@ simple_tactic: [
 | "notypeclasses" "refine" uconstr
 | "simple" "notypeclasses" "refine" uconstr
 | "solve_constraints"
-| "subst" LIST1 var
+| "subst" LIST1 hyp
 | "subst"
 | "simple" "subst"
 | "evar" test_lpar_id_colon "(" ident ":" lconstr ")"
@@ -1619,6 +1616,7 @@ simple_tactic: [
 | "convert_concl_no_check" constr
 | "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
 | "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident
+| "typeclasses" "eauto" "bfs" OPT int_or_var
 | "typeclasses" "eauto" OPT int_or_var
 | "head_of_constr" ident constr
 | "not_evar" constr
@@ -1792,7 +1790,7 @@ auto_using': [
 ]
 
 function_rec_definition_loc: [
-| Vernac.rec_definition      (* funind plugin *)
+| Vernac.fix_definition      (* funind plugin *)
 ]
 
 fun_scheme_arg: [
@@ -1811,7 +1809,7 @@ EXTRAARGS_natural: [
 
 occurrences: [
 | LIST1 integer
-| var
+| hyp
 ]
 
 glob: [
@@ -1929,12 +1927,12 @@ tactic_then_last: [
 |
 ]
 
-tactic_then_gen: [
-| ltac_expr5 "|" tactic_then_gen
+for_each_goal: [
+| ltac_expr5 "|" for_each_goal
 | ltac_expr5 ".." tactic_then_last
 | ".." tactic_then_last
 | ltac_expr5
-| "|" tactic_then_gen
+| "|" for_each_goal
 |
 ]
 
@@ -1950,7 +1948,7 @@ ltac_expr5: [
 ltac_expr4: [
 | ltac_expr3 ";" binder_tactic
 | ltac_expr3 ";" ltac_expr3
-| ltac_expr3 ";" tactic_then_locality tactic_then_gen "]"
+| ltac_expr3 ";" tactic_then_locality for_each_goal "]"
 | ltac_expr3
 ]
 
@@ -1966,7 +1964,7 @@ ltac_expr3: [
 | "infoH" ltac_expr3
 | "abstract" ltac_expr2
 | "abstract" ltac_expr2 "using" ident
-| selector ltac_expr3
+| "only" selector ":" ltac_expr3
 | ltac_expr2
 ]
 
@@ -1988,14 +1986,14 @@ ltac_expr1: [
 | "idtac" LIST0 message_token
 | failkw [ int_or_var | ] LIST0 message_token
 | simple_tactic
-| tactic_arg
-| reference LIST0 tactic_arg_compat
+| tactic_value
+| reference LIST0 tactic_arg
 | ltac_expr0
 ]
 
 ltac_expr0: [
 | "(" ltac_expr5 ")"
-| "[" ">" tactic_then_gen "]"
+| "[" ">" for_each_goal "]"
 | tactic_atom
 ]
 
@@ -2009,13 +2007,13 @@ binder_tactic: [
 | "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
@@ -2062,19 +2060,19 @@ let_clause: [
 ]
 
 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 "=>" ltac_expr5
-| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" ltac_expr5
+| LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr5
+| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr5
 | "_" "=>" ltac_expr5
 ]
 
@@ -2123,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" ":"
 ]
@@ -2358,7 +2352,7 @@ with_bindings: [
 |
 ]
 
-red_flags: [
+red_flag: [
 | "beta"
 | "iota"
 | "match"
@@ -2375,7 +2369,7 @@ delta_flag: [
 ]
 
 strategy_flag: [
-| LIST1 red_flags
+| LIST1 red_flag
 | delta_flag
 ]
 
@@ -2555,7 +2549,7 @@ field_mods: [
 | "(" LIST1 field_mod SEP "," ")"      (* ring plugin *)
 ]
 
-numnotoption: [
+numeral_modifier: [
 |
 | "(" "warning" "after" bignat ")"
 | "(" "abstract" "after" bignat ")"
@@ -2660,15 +2654,15 @@ 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: [
@@ -2799,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: [
@@ -2812,7 +2806,7 @@ syn_level: [
 ]
 
 tac2def_syn: [
-| "Notation" LIST1 sexpr syn_level ":=" tac2expr6      (* Ltac2 plugin *)
+| "Notation" LIST1 ltac2_scope syn_level ":=" tac2expr6      (* Ltac2 plugin *)
 ]
 
 lident: [
@@ -3034,24 +3028,24 @@ G_LTAC2_tactic_then_last: [
 |      (* Ltac2 plugin *)
 ]
 
-G_LTAC2_tactic_then_gen: [
-| tac2expr6 "|" G_LTAC2_tactic_then_gen      (* Ltac2 plugin *)
+G_LTAC2_for_each_goal: [
+| tac2expr6 "|" G_LTAC2_for_each_goal      (* Ltac2 plugin *)
 | tac2expr6 ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
 | ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
 | tac2expr6      (* Ltac2 plugin *)
-| "|" G_LTAC2_tactic_then_gen      (* 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 *)
@@ -3082,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 *)
 ]
 
@@ -3100,8 +3094,8 @@ 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: [
@@ -3129,13 +3123,13 @@ gmatch_rule: [
 | gmatch_pattern "=>" tac2expr6      (* 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: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index ff1efa5375..0827ccd193 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -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