Rename misc nonterminals

7 files changed, 31 insertions, 31 deletions

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 }