Rename misc nonterminals

21 files changed, 362 insertions, 421 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
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 297dc3a706..ddfa3a80bd 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -317,7 +317,7 @@ let pattern_of_string ?env s =
     | None -> Global.env ()
     | Some e -> e
   in
-  let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
+  let constr = Pcoq.parse_string Pcoq.Constr.cpattern s in
   let (_, pat) = Constrintern.intern_constr_pattern env (Evd.from_env env) constr in
   pat
 
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 5417a14e6d..aac43db672 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -11,7 +11,7 @@
 (** Generic arguments used by the extension mechanisms of several Coq ASTs. *)
 
 (** The route of a generic argument, from parsing to evaluation.
-In the following diagram, "object" can be ltac_expr, constr, tactic_arg, etc.
+In the following diagram, "object" can be ltac_expr, constr, tactic_value, etc.
 
 {% \begin{verbatim} %}
              parsing          in_raw                            out_raw
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index bfd1fed6f0..a4660bfe8b 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -82,9 +82,9 @@ let test_array_closing =
 GRAMMAR EXTEND Gram
   GLOBAL: binder_constr lconstr constr term
   universe_level universe_name sort sort_family
-  global constr_pattern lconstr_pattern Constr.ident
+  global constr_pattern cpattern Constr.ident
   closed_binder open_binders binder binders binders_fixannot
-  record_declaration typeclass_constraint pattern appl_arg type_cstr;
+  record_declaration typeclass_constraint pattern arg type_cstr;
   Constr.ident:
     [ [ id = Prim.ident -> { id } ] ]
   ;
@@ -97,7 +97,7 @@ GRAMMAR EXTEND Gram
   constr_pattern:
     [ [ c = constr -> { c } ] ]
   ;
-  lconstr_pattern:
+  cpattern:
     [ [ c = lconstr -> { c } ] ]
   ;
   sort:
@@ -135,7 +135,7 @@ GRAMMAR EXTEND Gram
   ;
   constr:
     [ [ c = term LEVEL "8" -> { c }
-      | "@"; f=global; i = univ_instance -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ]
+      | "@"; f=global; i = univ_annot -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ]
   ;
   term:
     [ "200" RIGHTA
@@ -152,8 +152,8 @@ GRAMMAR EXTEND Gram
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
-      [ f = term; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) }
-      | "@"; f = global; i = univ_instance; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) }
+      [ f = term; args = LIST1 arg -> { CAst.make ~loc @@ CApp((None,f),args) }
+      | "@"; f = global; i = univ_annot; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) }
       | "@"; lid = pattern_ident; args = LIST1 identref ->
         { let { CAst.loc = locid; v = id } = lid in
           let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
@@ -163,7 +163,7 @@ GRAMMAR EXTEND Gram
         { CAst.make ~loc @@ CAppExpl ((None, (qualid_of_ident ~loc ldots_var), None),[c]) } ]
     | "8" [ ]
     | "1" LEFTA
-      [ c = term; ".("; f = global; args = LIST0 appl_arg; ")" ->
+      [ c = term; ".("; f = global; args = LIST0 arg; ")" ->
         { CAst.make ~loc @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) }
       | c = term; ".("; "@"; f = global;
         args = LIST0 (term LEVEL "9"); ")" ->
@@ -171,7 +171,7 @@ GRAMMAR EXTEND Gram
       | c = term; "%"; key = IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ]
     | "0"
       [ c = atomic_constr -> { c }
-      | c = match_constr -> { c }
+      | c = term_match -> { c }
       | "("; c = term LEVEL "200"; ")" ->
         { (* Preserve parentheses around numerals so that constrintern does not
              collapse -(3) into the numeral -3. *)
@@ -184,7 +184,7 @@ GRAMMAR EXTEND Gram
         { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) }
       | "`{"; c = term LEVEL "200"; "}" ->
         { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
-      | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_instance ->
+      | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_annot ->
         { let t = Array.make (List.length ls) def in
           List.iteri (fun i e -> t.(i) <- e) ls;
           CAst.make ~loc @@ CArray(u, t, def, ty)
@@ -219,16 +219,16 @@ GRAMMAR EXTEND Gram
           | _, _ -> ty, c1 in
           CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1,
                  Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) }
-      | "let"; "fix"; fx = fix_decl; "in"; c = term LEVEL "200" ->
+      | "let"; "fix"; fx = fix_body; "in"; c = term LEVEL "200" ->
         { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_ as dcl)} = fx in
           let fix = CAst.make ?loc:locf @@ CFix (lid,[dcl]) in
           CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fix,None,c) }
-      | "let"; "cofix"; fx = cofix_decl; "in"; c = term LEVEL "200" ->
+      | "let"; "cofix"; fx = cofix_body; "in"; c = term LEVEL "200" ->
         { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_ as dcl)} = fx in
           let cofix = CAst.make ?loc:locf @@ CCoFix (lid,[dcl]) in
           CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,cofix,None,c) }
       | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ];
-        po = return_type; ":="; c1 = term LEVEL "200"; "in";
+        po = as_return_type; ":="; c1 = term LEVEL "200"; "in";
         c2 = term LEVEL "200" ->
         { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) }
       | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = term LEVEL "200";
@@ -244,19 +244,19 @@ GRAMMAR EXTEND Gram
         "in"; c2 = term LEVEL "200" ->
         { CAst.make ~loc @@
           CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc ([[p]], c2)]) }
-      | "if"; c = term LEVEL "200"; po = return_type;
+      | "if"; c = term LEVEL "200"; po = as_return_type;
         "then"; b1 = term LEVEL "200";
         "else"; b2 = term LEVEL "200" ->
         { CAst.make ~loc @@ CIf (c, po, b1, b2) }
       | "fix"; c = fix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CFix (id,dcls) }
       | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ]
   ;
-  appl_arg:
+  arg:
     [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) }
       | c=term LEVEL "9" -> { (c,None) } ] ]
   ;
   atomic_constr:
-    [ [ g = global; i = univ_instance -> { CAst.make ~loc @@ CRef (g,i) }
+    [ [ g = global; i = univ_annot -> { CAst.make ~loc @@ CRef (g,i) }
       | s = sort   -> { CAst.make ~loc @@  CSort s }
       | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPrim (String s) }
@@ -272,7 +272,7 @@ GRAMMAR EXTEND Gram
     [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l }
       | -> { [] } ] ]
   ;
-  univ_instance:
+  univ_annot:
     [ [ "@{"; l = LIST0 universe_level; "}" -> { Some l }
       | -> { None } ] ]
   ;
@@ -285,26 +285,26 @@ GRAMMAR EXTEND Gram
       | id = global -> { UNamed (GType id) } ] ]
   ;
   fix_decls:
-    [ [ dcl = fix_decl -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
-      | dcl = fix_decl; "with"; dcls = LIST1 fix_decl SEP "with"; "for"; id = identref ->
+    [ [ dcl = fix_body -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
+      | dcl = fix_body; "with"; dcls = LIST1 fix_body SEP "with"; "for"; id = identref ->
         { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
   ;
   cofix_decls:
-    [ [ dcl = cofix_decl -> { let (id,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
-      | dcl = cofix_decl; "with"; dcls = LIST1 cofix_decl SEP "with"; "for"; id = identref ->
+    [ [ dcl = cofix_body -> { let (id,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
+      | dcl = cofix_body; "with"; dcls = LIST1 cofix_body SEP "with"; "for"; id = identref ->
         { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
   ;
-  fix_decl:~loc @@ ExplByName id))
+  fix_body:
     [ [ id = identref; bl = binders_fixannot; ty = type_cstr; ":=";
         c = term LEVEL "200" ->
         { CAst.make ~loc (id,snd bl,fst bl,ty,c) } ] ]
   ;
-  cofix_decl:
+  cofix_body:
     [ [ id = identref; bl = binders; ty = type_cstr; ":=";
         c = term LEVEL "200" ->
         { CAst.make ~loc (id,bl,ty,c) } ] ]
   ;
-  match_constr:
+  term_match:
     [ [ "match"; ci = LIST1 case_item SEP ","; ty = OPT case_type; "with";
         br = branches; "end" -> { CAst.make ~loc @@ CCases(RegularStyle,ty,ci,br) } ] ]
   ;
@@ -317,7 +317,7 @@ GRAMMAR EXTEND Gram
   case_type:
     [ [ "return"; ty = term LEVEL "100" -> { ty } ] ]
   ;
-  return_type:
+  as_return_type:
     [ [ a = OPT [ na = OPT["as"; na = name -> { na } ];
                   ty = case_type -> { (na,ty) } ] ->
         { match a with
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index ce73cee3be..22b5e70311 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -321,7 +321,8 @@ module Constr =
     let sort_family = Entry.create "sort_family"
     let pattern = Entry.create "pattern"
     let constr_pattern = Entry.create "constr_pattern"
-    let lconstr_pattern = Entry.create "lconstr_pattern"
+    let cpattern = Entry.create "cpattern"
+    let lconstr_pattern = cpattern
     let closed_binder = Entry.create "closed_binder"
     let binder = Entry.create "binder"
     let binders = Entry.create "binders"
@@ -329,7 +330,8 @@ module Constr =
     let binders_fixannot = Entry.create "binders_fixannot"
     let typeclass_constraint = Entry.create "typeclass_constraint"
     let record_declaration = Entry.create "record_declaration"
-    let appl_arg = Entry.create "appl_arg"
+    let arg = Entry.create "arg"
+    let appl_arg = arg
     let type_cstr = Entry.create "type_cstr"
   end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ccdf8abeda..ce4c91d51f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -196,7 +196,9 @@ module Constr :
     val sort_family : Sorts.family Entry.t
     val pattern : cases_pattern_expr Entry.t
     val constr_pattern : constr_expr Entry.t
+    val cpattern : constr_expr Entry.t
     val lconstr_pattern : constr_expr Entry.t
+      [@@deprecated "Deprecated in 8.13; use 'cpattern' instead"]
     val closed_binder : local_binder_expr list Entry.t
     val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
     val binders : local_binder_expr list Entry.t (* list of binder *)
@@ -204,7 +206,9 @@ module Constr :
     val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t
     val typeclass_constraint : (lname * bool * constr_expr) Entry.t
     val record_declaration : constr_expr Entry.t
+    val arg : (constr_expr * explicitation CAst.t option) Entry.t
     val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t
+      [@@deprecated "Deprecated in 8.13; use 'arg' instead"]
     val type_cstr : constr_expr Entry.t
   end
 
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index bbc4df7dde..4b46e09e57 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -159,7 +159,7 @@ GRAMMAR EXTEND Gram
   GLOBAL: function_rec_definition_loc ;
 
   function_rec_definition_loc:
-    [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]]
+    [ [ g = Vernac.fix_definition -> { Loc.tag ~loc g } ]]
     ;
 
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index affcf814d7..c38a4dcd90 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -74,7 +74,7 @@ let hint = G_proofs.hint
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_arg command hint
+  GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_value command hint
           tactic_mode constr_may_eval constr_eval toplevel_selector
           term;
 
@@ -84,12 +84,12 @@ GRAMMAR EXTEND Gram
       | -> { [||] }
     ] ]
   ;
-  tactic_then_gen:
-    [ [ ta = ltac_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) }
+  for_each_goal:
+    [ [ ta = ltac_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (ta::first, last) }
       | ta = ltac_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) }
       | ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) }
       | ta = ltac_expr -> { ([ta], None) }
-      | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) }
+      | "|"; tg = for_each_goal -> { let (first,last) = tg in (TacId [] :: first, last) }
       | -> { ([TacId []], None) }
     ] ]
   ;
@@ -103,7 +103,7 @@ GRAMMAR EXTEND Gram
     | "4" LEFTA
       [ ta0 = ltac_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) }
       | ta0 = ltac_expr; ";"; ta1 = ltac_expr -> { TacThen (ta0,ta1) }
-      | ta0 = ltac_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> {
+      | ta0 = ltac_expr; ";"; l = tactic_then_locality; tg = for_each_goal; "]" -> {
           let (first,tail) = tg in
           match l , tail with
           | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
@@ -124,7 +124,7 @@ GRAMMAR EXTEND Gram
       | IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) }
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
         { TacAbstract (tc,Some s) }
-      | sel = selector; ta = ltac_expr -> { TacSelect (sel, ta) } ]
+      | IDENT "only"; sel = selector; ":"; ta = ltac_expr -> { TacSelect (sel, ta) } ]
 (*End of To do*)
     | "2" RIGHTA
       [ ta0 = ltac_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) }
@@ -150,12 +150,12 @@ GRAMMAR EXTEND Gram
       | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ];
           l = LIST0 message_token -> { TacFail (g,n,l) }
       | st = simple_tactic -> { st }
-      | a = tactic_arg -> { TacArg(CAst.make ~loc a) }
-      | r = reference; la = LIST0 tactic_arg_compat ->
+      | a = tactic_value -> { TacArg(CAst.make ~loc a) }
+      | r = reference; la = LIST0 tactic_arg ->
         { TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ]
     | "0"
       [ "("; a = ltac_expr; ")" -> { a }
-      | "["; ">"; tg = tactic_then_gen; "]" -> {
+      | "["; ">"; tg = for_each_goal; "]" -> {
           let (tf,tail) = tg in
           begin match tail with
           | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
@@ -176,14 +176,14 @@ GRAMMAR EXTEND Gram
           body = ltac_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ]
   ;
   (* Tactic arguments to the right of an application *)
-  tactic_arg_compat:
-    [ [ a = tactic_arg -> { a }
+  tactic_arg:
+    [ [ a = tactic_value -> { a }
       | c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) }
       (* Unambiguous entries: tolerated w/o "ltac:" modifier *)
       | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
   ;
   (* Can be used as argument and at toplevel in tactic expressions. *)
-  tactic_arg:
+  tactic_value:
     [ [ c = constr_eval -> { ConstrMayEval c }
       | IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l }
       | IDENT "type_term"; c=uconstr -> { TacPretype c }
@@ -232,11 +232,11 @@ GRAMMAR EXTEND Gram
   ;
   match_pattern:
     [ [ IDENT "context";  oid = OPT Constr.ident;
-          "["; pc = Constr.lconstr_pattern; "]" ->
+          "["; pc = Constr.cpattern; "]" ->
         { Subterm (oid, pc) }
-      | pc = Constr.lconstr_pattern -> { Term pc } ] ]
+      | pc = Constr.cpattern -> { Term pc } ] ]
   ;
-  match_hyps:
+  match_hyp:
     [ [ na = name; ":"; mp =  match_pattern -> { Hyp (na, mp) }
       | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) }
       | na = name; ":="; mpv = match_pattern ->
@@ -250,9 +250,9 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   match_context_rule:
-    [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
+    [ [ largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern;
         "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
-      | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
+      | "["; largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern;
         "]"; "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
       | "_"; "=>"; te = ltac_expr -> { All te } ] ]
   ;
@@ -314,15 +314,12 @@ GRAMMAR EXTEND Gram
         { let open Goal_select in
           Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ]
   ;
-  selector_body:
+  selector:
   [ [ l = range_selector_or_nth -> { l }
     | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ]
   ;
-  selector:
-    [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ]
-  ;
   toplevel_selector:
-    [ [ sel = selector_body; ":" -> { sel }
+    [ [ sel = selector; ":" -> { sel }
     |   "!"; ":" -> { Goal_select.SelectAlreadyFocused }
     |   IDENT "all"; ":" -> { Goal_select.SelectAll } ] ]
   ;
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 7b020c40ba..97d75261c5 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -320,7 +320,7 @@ GRAMMAR EXTEND Gram
   with_bindings:
     [ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ]
   ;
-  red_flags:
+  red_flag:
     [ [ IDENT "beta" -> { [FBeta] }
       | IDENT "iota" -> { [FMatch;FFix;FCofix] }
       | IDENT "match" -> { [FMatch] }
@@ -337,7 +337,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   strategy_flag:
-    [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) }
+    [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) }
       | d = delta_flag -> { all_with d }
     ] ]
   ;
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 1631215d58..94e398fe5d 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -37,7 +37,8 @@ let clause_dft_concl =
 
 
 (* Main entries for ltac *)
-let tactic_arg = Entry.create "tactic_arg"
+let tactic_value = Entry.create "tactic_value"
+let tactic_arg = tactic_value
 let ltac_expr = Entry.create "ltac_expr"
 let tactic_expr = ltac_expr
 let binder_tactic = Entry.create "binder_tactic"
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index a2424d4c60..3a4a081c93 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -31,7 +31,9 @@ val simple_tactic : raw_tactic_expr Entry.t
 val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
 val in_clause : Names.lident Locus.clause_expr Entry.t
 val clause_dft_concl : Names.lident Locus.clause_expr Entry.t
+val tactic_value : raw_tactic_arg Entry.t
 val tactic_arg : raw_tactic_arg Entry.t
+  [@@deprecated "Deprecated in 8.13; use 'tactic_value' instead"]
 val ltac_expr : raw_tactic_expr Entry.t
 val tactic_expr : raw_tactic_expr Entry.t
   [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"]
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 159ca678e9..a05b36c1b4 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -420,7 +420,7 @@ let create_ltac_quotation name cast (e, l) =
   in
   let action _ v _ _ _ loc = cast (Some loc, v) in
   let gram = (level, assoc, [Pcoq.Production.make rule action]) in
-  Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]}
+  Pcoq.grammar_extend Pltac.tactic_value {pos=None; data=[gram]}
 
 (** Command *)
 
@@ -558,7 +558,7 @@ let () =
     AnyEntry Pltac.ltac_expr;
     AnyEntry Pltac.binder_tactic;
     AnyEntry Pltac.simple_tactic;
-    AnyEntry Pltac.tactic_arg;
+    AnyEntry Pltac.tactic_value;
   ] in
   register_grammars_by_name "tactic" entries
 
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index c030925ea9..93d91abea3 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -31,7 +31,7 @@ let warn_deprecated_numeral_notation =
 
 }
 
-VERNAC ARGUMENT EXTEND numnotoption
+VERNAC ARGUMENT EXTEND numeral_modifier
   PRINTED BY { pr_numnot_option }
 | [ ] -> { Nop }
 | [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) }
@@ -40,11 +40,11 @@ END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
   | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":"
-      ident(sc) numnotoption(o) ] ->
+      ident(sc) numeral_modifier(o) ] ->
 
     { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
   | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
-      ident(sc) numnotoption(o) ] ->
+      ident(sc) numeral_modifier(o) ] ->
 
     { warn_deprecated_numeral_notation ();
       vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index cc2cdf7ef8..024722cf1e 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -80,7 +80,7 @@ let tac2def_syn = Entry.create "tac2def_syn"
 let tac2def_mut = Entry.create "tac2def_mut"
 let tac2mode = Entry.create "ltac2_command"
 
-let ltac1_expr = Pltac.ltac_expr
+let ltac_expr = Pltac.ltac_expr
 let tac2expr_in_env = Tac2entries.Pltac.tac2expr_in_env
 
 let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)
@@ -210,15 +210,15 @@ GRAMMAR EXTEND Gram
       | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_constr c }
       | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_open_constr c }
       | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c }
-      | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> { inj_pattern loc c }
+      | IDENT "pattern"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c }
       | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c }
       | IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid }
       | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid }
     ] ]
   ;
   ltac1_expr_in_env:
-    [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac1_expr -> { ids, e }
-      | e = ltac1_expr -> { [], e }
+    [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac_expr -> { ids, e }
+      | e = ltac_expr -> { [], e }
     ] ]
   ;
   tac2expr_in_env :
@@ -361,11 +361,11 @@ GRAMMAR EXTEND Gram
       | id = Prim.ident -> { CAst.make ~loc (Some id) }
     ] ]
   ;
-  sexpr:
+  ltac2_scope:
     [ [ s = Prim.string -> { SexprStr (CAst.make ~loc s) }
       | n = Prim.integer -> { SexprInt (CAst.make ~loc n) }
       | id = syn_node -> { SexprRec (loc, id, []) }
-      | id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" ->
+      | id = syn_node; "("; tok = LIST1 ltac2_scope SEP "," ; ")" ->
         { SexprRec (loc, id, tok) }
     ] ]
   ;
@@ -375,7 +375,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   tac2def_syn:
-    [ [ "Notation"; toks = LIST1 sexpr; n = syn_level; ":=";
+    [ [ "Notation"; toks = LIST1 ltac2_scope; n = syn_level; ":=";
         e = tac2expr ->
         { StrSyn (toks, n, e) }
     ] ]
@@ -658,22 +658,22 @@ GRAMMAR EXTEND Gram
       | -> { [] }
     ] ]
   ;
-  tactic_then_gen:
-    [ [ ta = tac2expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (Some ta :: first, last) }
+  for_each_goal:
+    [ [ ta = tac2expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (Some ta :: first, last) }
       | ta = tac2expr; ".."; l = tactic_then_last -> { ([], Some (Some ta, l)) }
       | ".."; l = tactic_then_last -> { ([], Some (None, l)) }
       | ta = tac2expr -> { ([Some ta], None) }
-      | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (None :: first, last) }
+      | "|"; tg = for_each_goal -> { let (first,last) = tg in (None :: first, last) }
       | -> { ([None], None) }
     ] ]
   ;
   q_dispatch:
-    [ [ d = tactic_then_gen -> { CAst.make ~loc d } ] ]
+    [ [ d = for_each_goal -> { CAst.make ~loc d } ] ]
   ;
   q_occurrences:
     [ [ occs = occs -> { occs } ] ]
   ;
-  red_flag:
+  ltac2_red_flag:
     [ [ IDENT "beta" -> { CAst.make ~loc @@ QBeta }
       | IDENT "iota" -> { CAst.make ~loc @@ QIota }
       | IDENT "match" -> { CAst.make ~loc @@ QMatch }
@@ -702,7 +702,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   strategy_flag:
-    [ [ s = LIST1 red_flag -> { CAst.make ~loc s }
+    [ [ s = LIST1 ltac2_red_flag -> { CAst.make ~loc s }
       | d = delta_flag ->
       { CAst.make ~loc
           [CAst.make ~loc QBeta; CAst.make ~loc QIota; CAst.make ~loc QZeta; d] }
@@ -721,8 +721,8 @@ GRAMMAR EXTEND Gram
   ;
   match_pattern:
     [ [ IDENT "context";  id = OPT Prim.ident;
-          "["; pat = Constr.lconstr_pattern; "]" -> { CAst.make ~loc @@ QConstrMatchContext (id, pat) }
-      | pat = Constr.lconstr_pattern -> { CAst.make ~loc @@ QConstrMatchPattern pat } ] ]
+          "["; pat = Constr.cpattern; "]" -> { CAst.make ~loc @@ QConstrMatchContext (id, pat) }
+      | pat = Constr.cpattern -> { CAst.make ~loc @@ QConstrMatchPattern pat } ] ]
   ;
   match_rule:
     [ [ mp = match_pattern; "=>"; tac = tac2expr ->
@@ -752,12 +752,12 @@ GRAMMAR EXTEND Gram
         { CAst.make ~loc @@ (mp, tac) }
     ] ]
   ;
-  gmatch_list:
+  goal_match_list:
     [ [ mrl = LIST1 gmatch_rule SEP "|" -> { CAst.make ~loc @@ mrl }
       | "|"; mrl = LIST1 gmatch_rule SEP "|" -> { CAst.make ~loc @@ mrl } ] ]
   ;
   q_goal_matching:
-    [ [ m = gmatch_list -> { m } ] ]
+    [ [ m = goal_match_list -> { m } ] ]
   ;
   move_location:
     [ [ "at"; IDENT "top" -> { CAst.make ~loc @@ QMoveFirst }
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 4c08cf7f79..3d6a93c888 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -48,7 +48,7 @@ let assumption_token = Entry.create "assumption_token"
 let def_body = Entry.create "def_body"
 let decl_notations = Entry.create "decl_notations"
 let record_field = Entry.create "record_field"
-let of_type_with_opt_coercion = Entry.create "of_type_with_opt_coercion"
+let of_type = Entry.create "of_type"
 let section_subset_expr = Entry.create "section_subset_expr"
 let scope_delimiter = Entry.create "scope_delimiter"
 let syntax_modifiers = Entry.create "syntax_modifiers"
@@ -113,10 +113,10 @@ GRAMMAR EXTEND Gram
     ]
   ;
   attribute:
-    [ [ k = ident ; v = attribute_value -> { Names.Id.to_string k, v } ]
+    [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v } ]
     ]
   ;
-  attribute_value:
+  attr_value:
     [ [ "=" ; v = string -> { VernacFlagLeaf v }
       | "(" ; a = attribute_list ; ")" -> { VernacFlagList a }
       | -> { VernacFlagEmpty } ]
@@ -196,8 +196,8 @@ let name_of_ident_decl : ident_decl -> name_decl =
 
 (* Gallina declarations *)
 GRAMMAR EXTEND Gram
-  GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type_with_opt_coercion
-    record_field decl_notations rec_definition ident_decl univ_decl;
+  GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type
+    record_field decl_notations fix_definition ident_decl univ_decl;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
@@ -219,13 +219,13 @@ GRAMMAR EXTEND Gram
       (* Gallina inductive declarations *)
       | f = finite_token; indl = LIST1 inductive_definition SEP "with" ->
           { VernacInductive (f, indl) }
-      | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+      | "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
           { VernacFixpoint (NoDischarge, recs) }
-      | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+      | IDENT "Let"; "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
           { VernacFixpoint (DoDischarge, recs) }
-      | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+      | "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
           { VernacCoFixpoint (NoDischarge, corecs) }
-      | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+      | IDENT "Let"; "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
           { VernacCoFixpoint (DoDischarge, corecs) }
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
@@ -339,7 +339,7 @@ GRAMMAR EXTEND Gram
   ;
   (* Inductives and records *)
   opt_constructors_or_fields:
-    [ [ ":="; lc = constructor_list_or_record_decl -> { lc }
+    [ [ ":="; lc = constructors_or_record -> { lc }
       | -> { RecordDecl (None, []) } ] ]
   ;
   inductive_definition:
@@ -349,7 +349,7 @@ GRAMMAR EXTEND Gram
         lc=opt_constructors_or_fields; ntn = decl_notations ->
            { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ]
   ;
-  constructor_list_or_record_decl:
+  constructors_or_record:
     [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
       | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" ->
           { Constructors ((c id)::l) }
@@ -369,7 +369,7 @@ GRAMMAR EXTEND Gram
       |  -> { false } ] ]
   ;
   (* (co)-fixpoints *)
-  rec_definition:
+  fix_definition:
     [ [ id_decl = ident_decl;
         bl = binders_fixannot;
         rtype = type_cstr;
@@ -378,7 +378,7 @@ GRAMMAR EXTEND Gram
             {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations}
           } ] ]
   ;
-  corec_definition:
+  cofix_definition:
     [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
         body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations ->
         { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations}
@@ -427,10 +427,10 @@ GRAMMAR EXTEND Gram
       | -> { [] }
     ] ]
   ;
-  record_binder_body:
-    [ [ l = binders; oc = of_type_with_opt_coercion;
+  field_body:
+    [ [ l = binders; oc = of_type;
          t = lconstr -> { fun id -> (oc,AssumExpr (id,l,t)) }
-      | l = binders; oc = of_type_with_opt_coercion;
+      | l = binders; oc = of_type;
          t = lconstr; ":="; b = lconstr -> { fun id ->
            (oc,DefExpr (id,l,b,Some t)) }
       | l = binders; ":="; b = lconstr -> { fun id ->
@@ -442,22 +442,22 @@ GRAMMAR EXTEND Gram
   ;
   record_binder:
     [ [ id = name -> { (NoInstance,AssumExpr(id, [], CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
-      | id = name; f = record_binder_body -> { f id } ] ]
+      | id = name; f = field_body -> { f id } ] ]
   ;
   assum_list:
-    [ [ bl = LIST1 assum_coe -> { bl } | b = simple_assum_coe -> { [b] } ] ]
+    [ [ bl = LIST1 assum_coe -> { bl } | b = assumpt -> { [b] } ] ]
   ;
   assum_coe:
-    [ [ "("; a = simple_assum_coe; ")" -> { a } ] ]
+    [ [ "("; a = assumpt; ")" -> { a } ] ]
   ;
-  simple_assum_coe:
-    [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr ->
+  assumpt:
+    [ [ idl = LIST1 ident_decl; oc = of_type; c = lconstr ->
         { (oc <> NoInstance,(idl,c)) } ] ]
   ;
 
   constructor_type:
     [[ l = binders;
-      t= [ coe = of_type_with_opt_coercion; c = lconstr ->
+      t= [ coe = of_type; c = lconstr ->
                     { fun l id -> (coe <> NoInstance,(id,mkProdCN ~loc l c)) }
             |  ->
                  { fun l id -> (false,(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ]
@@ -468,7 +468,7 @@ GRAMMAR EXTEND Gram
   constructor:
     [ [ id = identref; c=constructor_type -> { c id } ] ]
   ;
-  of_type_with_opt_coercion:
+  of_type:
     [ [   ":>" -> { BackInstance }
         | ":"; ">" -> { BackInstance }
         | ":" -> { NoInstance } ] ]
@@ -707,13 +707,13 @@ GRAMMAR EXTEND Gram
 
       (* Arguments *)
       | IDENT "Arguments"; qid = smart_global;
-        args = LIST0 argument_spec_block;
+        args = LIST0 arg_specs;
         more_implicits = OPT
           [ ","; impl = LIST1
-            [ impl = LIST0 more_implicits_block -> { List.flatten impl } ]
+            [ impl = LIST0 implicits_alt -> { List.flatten impl } ]
             SEP "," -> { impl }
           ];
-        mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] ->
+        mods = OPT [ ":"; l = LIST1 args_modifier SEP "," -> { l } ] ->
          { let mods = match mods with None -> [] | Some l -> List.flatten l in
          let more_implicits = Option.default [] more_implicits in
          VernacArguments (qid, List.flatten args, more_implicits, mods) }
@@ -732,7 +732,7 @@ GRAMMAR EXTEND Gram
                   idl = LIST1 identref -> { Some idl } ] ->
              { VernacGeneralizable gen } ] ]
   ;
-  arguments_modifier:
+  args_modifier:
     [ [ IDENT "simpl"; IDENT "nomatch" -> { [`ReductionDontExposeCase] }
       | IDENT "simpl"; IDENT "never" -> { [`ReductionNeverUnfold] }
       | IDENT "default"; IDENT "implicits" -> { [`DefaultImplicits] }
@@ -757,7 +757,7 @@ GRAMMAR EXTEND Gram
     ]
   ];
   (* List of arguments implicit status, scope, modifiers *)
-  argument_spec_block: [
+  arg_specs: [
     [ item = argument_spec ->
       { let name, recarg_like, notation_scope = item in
       [RealArg { name=name; recarg_like=recarg_like;
@@ -791,8 +791,8 @@ GRAMMAR EXTEND Gram
                  implicit_status = MaxImplicit}) items }
     ]
   ];
-  (* Same as [argument_spec_block], but with only implicit status and names *)
-  more_implicits_block: [
+  (* Same as [arg_specs], but with only implicit status and names *)
+  implicits_alt: [
     [ name = name -> { [(name.CAst.v, Explicit)] }
     | "["; items = LIST1 name; "]" ->
        { List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items }
@@ -826,9 +826,9 @@ GRAMMAR EXTEND Gram
   GLOBAL: command query_command class_rawexpr gallina_ext search_query search_queries;
 
   gallina_ext:
-    [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting ->
+    [ [ IDENT "Export"; "Set"; table = setting_name; v = option_setting ->
         { VernacSetOption (true, table, v) }
-      | IDENT "Export"; IDENT "Unset"; table = option_table ->
+      | IDENT "Export"; IDENT "Unset"; table = setting_name ->
           { VernacSetOption (true, table, OptionUnset) }
     ] ];
 
@@ -885,12 +885,12 @@ GRAMMAR EXTEND Gram
           { VernacAddMLPath dir }
 
       (* For acting on parameter tables *)
-      | "Set"; table = option_table; v = option_setting ->
+      | "Set"; table = setting_name; v = option_setting ->
           { VernacSetOption (false, table, v) }
-      | IDENT "Unset"; table = option_table ->
+      | IDENT "Unset"; table = setting_name ->
           { VernacSetOption (false, table, OptionUnset) }
 
-      | IDENT "Print"; IDENT "Table"; table = option_table ->
+      | IDENT "Print"; IDENT "Table"; table = setting_name ->
           { VernacPrintOption table }
 
       | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 table_value
@@ -902,9 +902,9 @@ GRAMMAR EXTEND Gram
       | IDENT "Add"; table = IDENT; v = LIST1 table_value ->
           { VernacAddOption ([table], v) }
 
-      | IDENT "Test"; table = option_table; "for"; v = LIST1 table_value
+      | IDENT "Test"; table = setting_name; "for"; v = LIST1 table_value
         -> { VernacMemOption (table, v) }
-      | IDENT "Test"; table = option_table ->
+      | IDENT "Test"; table = setting_name ->
           { VernacPrintOption table }
 
       | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value
@@ -1006,7 +1006,7 @@ GRAMMAR EXTEND Gram
     [ [ id = global   -> { Goptions.QualidRefValue id }
       | s  = STRING   -> { Goptions.StringRefValue s } ] ]
   ;
-  option_table:
+  setting_name:
     [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
   ;
   ne_in_or_out_modules:
@@ -1191,10 +1191,10 @@ GRAMMAR EXTEND Gram
           | s, None -> SetFormat ("text",s) end }
       | x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at";
         lev = level -> { SetItemLevel (x::l,None,lev) }
-      | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind ->
+      | x = IDENT; "at"; lev = level; b = OPT binder_interp ->
         { SetItemLevel ([x],b,lev) }
-      | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) }
-      | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
+      | x = IDENT; b = binder_interp -> { SetItemLevel ([x],Some b,DefaultLevel) }
+      | x = IDENT; typ = explicit_subentry -> { SetEntryType (x,typ) }
     ] ]
   ;
   syntax_modifiers:
@@ -1202,18 +1202,18 @@ GRAMMAR EXTEND Gram
       | -> { [] }
     ] ]
   ;
-  syntax_extension_type:
+  explicit_subentry:
     [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
       | IDENT "bigint" -> { ETBigint }
       | IDENT "binder" -> { ETBinder true }
       | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
-      | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
+      | IDENT "constr"; n = at_level_opt; b = OPT binder_interp -> { ETConstr (InConstrEntry,b,n) }
       | IDENT "pattern" -> { ETPattern (false,None) }
       | IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
       | IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
       | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
       | IDENT "closed"; IDENT "binder" -> { ETBinder false }
-      | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT constr_as_binder_kind ->
+      | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT binder_interp ->
            { ETConstr (InCustomEntry x,b,n) }
     ] ]
   ;
@@ -1221,7 +1221,7 @@ GRAMMAR EXTEND Gram
     [ [ "at"; n = level -> { n }
       | -> { DefaultLevel } ] ]
   ;
-  constr_as_binder_kind:
+  binder_interp:
     [ [ "as"; IDENT "ident" -> { Notation_term.AsIdent }
       | "as"; IDENT "pattern" -> { Notation_term.AsIdentOrPattern }
       | "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ]
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index c9f68eed57..a7de34dd09 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -43,7 +43,8 @@ module Vernac_ =
     let command = Entry.create "command"
     let syntax = Entry.create "syntax_command"
     let vernac_control = Entry.create "Vernac.vernac_control"
-    let rec_definition = Entry.create "Vernac.rec_definition"
+    let fix_definition = Entry.create "Vernac.fix_definition"
+    let rec_definition = fix_definition
     let red_expr = Entry.create "red_expr"
     let hint_info = Entry.create "hint_info"
     (* Main vernac entry *)
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 8ab4af7d48..dac6877cb3 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -25,7 +25,9 @@ module Vernac_ :
     val command : vernac_expr Entry.t
     val syntax : vernac_expr Entry.t
     val vernac_control : vernac_control Entry.t
+    val fix_definition : fixpoint_expr Entry.t
     val rec_definition : fixpoint_expr Entry.t
+      [@@deprecated "Deprecated in 8.13; use 'fix_definition' instead"]
     val noedit_mode : vernac_expr Entry.t
     val command_entry : vernac_expr Entry.t
     val main_entry : vernac_control option Entry.t