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

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

13 files changed, 125 insertions, 122 deletions

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index bbc4df7dde..ca6ae150a7 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -147,19 +147,19 @@ END
 module Vernac = Pvernac.Vernac_
 module Tactic = Pltac
 
-let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) =
-  Genarg.create_arg "function_rec_definition_loc"
+let (wit_function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) =
+  Genarg.create_arg "function_fix_definition"
 
-let function_rec_definition_loc =
-  Pcoq.create_generic_entry2 "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
+let function_fix_definition =
+  Pcoq.create_generic_entry2 "function_fix_definition" (Genarg.rawwit wit_function_fix_definition)
 
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: function_rec_definition_loc ;
+  GLOBAL: function_fix_definition ;
 
-  function_rec_definition_loc:
-    [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]]
+  function_fix_definition:
+    [ [ g = Vernac.fix_definition -> { Loc.tag ~loc g } ]]
     ;
 
 END
@@ -168,7 +168,7 @@ END
 
 let () =
   let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
-  Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
+  Pptactic.declare_extra_vernac_genarg_pprule wit_function_fix_definition raw_printer
 
 let is_proof_termination_interactively_checked recsl =
   List.exists (function
@@ -196,7 +196,7 @@ let is_interactive recsl =
 }
 
 VERNAC COMMAND EXTEND Function STATE CUSTOM
-| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+| ["Function" ne_function_fix_definition_list_sep(recsl,"with")]
     => { classify_funind recsl }
     -> {
          if is_interactive recsl then
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index ad4374dba3..ff4a82f864 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -41,7 +41,7 @@ let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simpl
 let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
 let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
-  Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5)
+  Tacentries.create_ltac_quotation "ltac" inject (Pltac.ltac_expr, Some 5)
 
 (** Backward-compatible tactic notation entry names *)
 
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 2d74323689..c38a4dcd90 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -74,22 +74,22 @@ let hint = G_proofs.hint
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: tactic tacdef_body tactic_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
-          operconstr;
+          term;
 
   tactic_then_last:
-    [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" ->
+    [ [ "|"; lta = LIST0 (OPT ltac_expr) SEP "|" ->
         { Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) }
       | -> { [||] }
     ] ]
   ;
-  tactic_then_gen:
-    [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) }
-      | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) }
+  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 = tactic_expr -> { ([ta], None) }
-      | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) }
+      | ta = ltac_expr -> { ([ta], None) }
+      | "|"; tg = for_each_goal -> { let (first,last) = tg in (TacId [] :: first, last) }
       | -> { ([TacId []], None) }
     ] ]
   ;
@@ -97,13 +97,13 @@ GRAMMAR EXTEND Gram
                            for [TacExtend] *)
   [ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ]
   ;
-  tactic_expr:
+  ltac_expr:
     [ "5" RIGHTA
       [ te = binder_tactic -> { te } ]
     | "4" LEFTA
-      [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) }
-      | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) }
-      | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> {
+      [ 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 = 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))
@@ -111,51 +111,51 @@ GRAMMAR EXTEND Gram
           | false , None -> TacThen (ta0,TacDispatch first)
           | true  , None -> TacThens (ta0,first) } ]
     | "3" RIGHTA
-      [ IDENT "try"; ta = tactic_expr -> { TacTry ta }
-      | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) }
-      | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) }
-      | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) }
-      | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta }
-      | IDENT "progress"; ta = tactic_expr -> { TacProgress ta }
-      | IDENT "once"; ta = tactic_expr -> { TacOnce ta }
-      | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta }
-      | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta }
+      [ IDENT "try"; ta = ltac_expr -> { TacTry ta }
+      | IDENT "do"; n = int_or_var; ta = ltac_expr -> { TacDo (n,ta) }
+      | IDENT "timeout"; n = int_or_var; ta = ltac_expr -> { TacTimeout (n,ta) }
+      | IDENT "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) }
+      | IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta }
+      | IDENT "progress"; ta = ltac_expr -> { TacProgress ta }
+      | IDENT "once"; ta = ltac_expr -> { TacOnce ta }
+      | IDENT "exactly_once"; ta = ltac_expr -> { TacExactlyOnce ta }
+      | IDENT "infoH"; ta = ltac_expr -> { TacShowHyps ta }
 (*To do: put Abstract in Refiner*)
       | IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) }
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
         { TacAbstract (tc,Some s) }
-      | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ]
+      | IDENT "only"; sel = selector; ":"; ta = ltac_expr -> { TacSelect (sel, ta) } ]
 (*End of To do*)
     | "2" RIGHTA
-      [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) }
-      | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) }
-      | IDENT "tryif" ; ta = tactic_expr ;
-              "then" ; tat = tactic_expr ;
-              "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) }
-      | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) }
-      | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ]
+      [ ta0 = ltac_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) }
+      | ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { TacOr (ta0,ta1) }
+      | IDENT "tryif" ; ta = ltac_expr ;
+              "then" ; tat = ltac_expr ;
+              "else" ; tae = ltac_expr -> { TacIfThenCatch(ta,tat,tae) }
+      | ta0 = ltac_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) }
+      | ta0 = ltac_expr; "||"; ta1 = ltac_expr -> { TacOrelse (ta0,ta1) } ]
     | "1" RIGHTA
       [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
           { TacMatchGoal (b,false,mrl) }
       | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
         mrl = match_context_list; "end" ->
           { TacMatchGoal (b,true,mrl) }
-      |	b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
+      |	b = match_key; c = ltac_expr; "with"; mrl = match_list; "end" ->
           { TacMatch (b,c,mrl) }
-      | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+      | IDENT "first" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
           { TacFirst l }
-      | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+      | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
           { TacSolve l }
       | IDENT "idtac"; l = LIST0 message_token -> { TacId l }
       | 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 = tactic_expr; ")" -> { a }
-      | "["; ">"; tg = tactic_then_gen; "]" -> {
+      [ "("; a = ltac_expr; ")" -> { a }
+      | "["; ">"; tg = for_each_goal; "]" -> {
           let (tf,tail) = tg in
           begin match tail with
           | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
@@ -166,24 +166,24 @@ GRAMMAR EXTEND Gram
   failkw:
   [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ]
   ;
-  (* binder_tactic: level 5 of tactic_expr *)
+  (* binder_tactic: level 5 of ltac_expr *)
   binder_tactic:
     [ RIGHTA
-      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" ->
           { TacFun (it,body) }
       | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ];
           llc = LIST1 let_clause SEP "with"; "in";
-          body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ]
+          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 }
@@ -223,20 +223,20 @@ GRAMMAR EXTEND Gram
       | l = ident -> { Name.Name l } ] ]
   ;
   let_clause:
-    [ [ idr = identref; ":="; te = tactic_expr ->
+    [ [ idr = identref; ":="; te = ltac_expr ->
          { (CAst.map (fun id -> Name id) idr, arg_of_expr te) }
-      | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr ->
+      | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = ltac_expr ->
          { (na, arg_of_expr te) }
-      | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
+      | idr = identref; args = LIST1 input_fun; ":="; te = ltac_expr ->
          { (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ]
   ;
   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,19 +250,19 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   match_context_rule:
-    [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
-        "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
-      | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
-        "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
-      | "_"; "=>"; te = tactic_expr -> { All te } ] ]
+    [ [ largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern;
+        "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
+      | "["; largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern;
+        "]"; "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
+      | "_"; "=>"; te = ltac_expr -> { All te } ] ]
   ;
   match_context_list:
     [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl }
       | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ]
   ;
   match_rule:
-    [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) }
-      | "_"; "=>"; te = tactic_expr -> { All te } ] ]
+    [ [ mp = match_pattern; "=>"; te = ltac_expr -> { Pat ([],mp,te) }
+      | "_"; "=>"; te = ltac_expr -> { All te } ] ]
   ;
   match_list:
     [ [ mrl = LIST1 match_rule SEP "|" -> { mrl }
@@ -282,13 +282,13 @@ GRAMMAR EXTEND Gram
   (* Definitions for tactics *)
   tacdef_body:
     [ [ name = Constr.global; it=LIST1 input_fun;
-        redef = ltac_def_kind; body = tactic_expr ->
+        redef = ltac_def_kind; body = ltac_expr ->
         { if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
           else
             let id = reference_to_id name in
             Tacexpr.TacticDefinition (id, TacFun (it, body)) }
       | name = Constr.global; redef = ltac_def_kind;
-        body = tactic_expr ->
+        body = ltac_expr ->
         { if redef then Tacexpr.TacticRedefinition (name, body)
           else
             let id = reference_to_id name in
@@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   tactic:
-    [ [ tac = tactic_expr -> { tac } ] ]
+    [ [ tac = ltac_expr -> { tac } ] ]
   ;
 
   range_selector:
@@ -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 } ] ]
   ;
@@ -343,8 +340,8 @@ GRAMMAR EXTEND Gram
         tac = Pltac.tactic ->
         { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
   ;
-  operconstr: LEVEL "0"
-    [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
+  term: LEVEL "0"
+    [ [ IDENT "ltac"; ":"; "("; tac = Pltac.ltac_expr; ")" ->
         { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
           CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ]
   ;
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index c186a83a5c..97d75261c5 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -291,7 +291,7 @@ GRAMMAR EXTEND Gram
   ;
   simple_intropattern:
     [ [ pat = simple_intropattern_closed;
-        l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] ->
+        l = LIST0 ["%"; c = term LEVEL "0" -> { c } ] ->
           { let {CAst.loc=loc0;v=pat} = pat in
           let f c pat =
             let loc1 = Constrexpr_ops.constr_loc c in
@@ -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 }
     ] ]
   ;
@@ -460,7 +460,7 @@ GRAMMAR EXTEND Gram
     [ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ]
   ;
   by_tactic:
-    [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac }
+    [ [ "by"; tac = ltac_expr LEVEL "3" -> { Some tac }
     | -> { None } ] ]
   ;
   rewriter :
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index b7b54143df..94e398fe5d 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -37,8 +37,10 @@ let clause_dft_concl =
 
 
 (* Main entries for ltac *)
-let tactic_arg = Entry.create "tactic_arg"
-let tactic_expr = Entry.create "tactic_expr"
+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"
 
 let tactic = Entry.create "tactic"
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 8565c4b4d6..3a4a081c93 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -31,8 +31,12 @@ 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"]
 val binder_tactic : raw_tactic_expr Entry.t
 val tactic : raw_tactic_expr Entry.t
 val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 6a9fb5c2ea..5e199dad62 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** This module implements pretty-printers for tactic_expr syntactic
+(** This module implements pretty-printers for ltac_expr syntactic
     objects and their subcomponents. *)
 
 open Genarg
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 6823b6411f..a05b36c1b4 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -33,7 +33,7 @@ type argument = Genarg.ArgT.any Extend.user_symbol
 
 let atactic n =
   if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
-  else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
+  else Pcoq.Symbol.nterml Pltac.ltac_expr (string_of_int n)
 
 type entry_name = EntryName :
   'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name
@@ -116,7 +116,7 @@ let get_tactic_entry n =
   else if Int.equal n 5 then
     Pltac.binder_tactic, None
   else if 1<=n && n<5 then
-    Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n))
+    Pltac.ltac_expr, Some (Gramlib.Gramext.Level (string_of_int n))
   else
     user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
 
@@ -383,7 +383,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods =
   in
   List.iteri iter (List.rev prods);
   (* We call [extend_atomic_tactic] only for "basic tactics" (the ones
-     at tactic_expr level 0) *)
+     at ltac_expr level 0) *)
   if Int.equal level 0 then extend_atomic_tactic name prods
 
 (**********************************************************************)
@@ -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 *)
 
@@ -555,10 +555,10 @@ let print_located_tactic qid =
 
 let () =
   let entries = [
-    AnyEntry Pltac.tactic_expr;
+    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/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 22b9abda20..7728415ddd 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1997,7 +1997,7 @@ let interp_tac_gen lfun avoid_ids debug t =
 let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t
 
 (* MUST be marshallable! *)
-type tactic_expr = {
+type ltac_expr = {
   global: bool;
   ast:  Tacexpr.raw_tactic_expr;
 }
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index dba9c938ec..fe3079198c 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -126,12 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
 val interp : raw_tactic_expr -> unit Proofview.tactic
 
 (** Hides interpretation for pretty-print *)
-type tactic_expr = {
+type ltac_expr = {
   global: bool;
   ast:  Tacexpr.raw_tactic_expr;
 }
 
-val hide_interp : tactic_expr -> ComTactic.interpretable
+val hide_interp : ltac_expr -> ComTactic.interpretable
 
 (** Internals that can be useful for syntax extensions. *)
 
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 7b584b5159..70dab585bf 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -100,7 +100,7 @@ ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
 END
 GRAMMAR EXTEND Gram
   GLOBAL: ssrtacarg;
-  ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]];
+  ssrtacarg: [[ tac = ltac_expr LEVEL "5" -> { tac } ]];
 END
 
 (* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *)
@@ -108,7 +108,7 @@ ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
 END
 GRAMMAR EXTEND Gram
   GLOBAL: ssrtac3arg;
-  ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]];
+  ssrtac3arg: [[ tac = ltac_expr LEVEL "3" -> { tac } ]];
 END
 
 {
@@ -1337,7 +1337,7 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde
 GRAMMAR EXTEND Gram
   GLOBAL: ssrbinder;
   ssrbinder: [
-  [  ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> {
+  [  ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> {
      (FwdPose, [BFvar]),
      CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
   ];
@@ -1594,18 +1594,18 @@ GRAMMAR EXTEND Gram
     | n = Prim.natural -> { ArgArg (check_index ~loc n) }
     ] ];
   ssrswap: [[ IDENT "first" -> { loc, true } | IDENT "last" -> { loc, false } ]];
-  ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> { tac } ]];
+  ssrorelse: [[ "||"; tac = ltac_expr LEVEL "2" -> { tac } ]];
   ssrseqarg: [
     [ arg = ssrswap -> { noindex, swaptacarg arg }
     | i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> { i, (tac, def) }
     | i = ssrseqidx; arg = ssrswap -> { i, swaptacarg arg }
-    | tac = tactic_expr LEVEL "3" -> { noindex, (mk_hint tac, None) }
+    | tac = ltac_expr LEVEL "3" -> { noindex, (mk_hint tac, None) }
     ] ];
 END
 
 {
 
-let tactic_expr = Pltac.tactic_expr
+let ltac_expr = Pltac.ltac_expr
 
 }
 
@@ -1688,9 +1688,9 @@ let tclintros_expr ?loc tac ipats =
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: tactic_expr;
-  tactic_expr: LEVEL "1" [ RIGHTA
-    [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
+  GLOBAL: ltac_expr;
+  ltac_expr: LEVEL "1" [ RIGHTA
+    [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
     ] ];
 END
 
@@ -1704,9 +1704,9 @@ END
 (* (Removing user-specified parentheses is dubious anyway).          *)
 
 GRAMMAR EXTEND Gram
-  GLOBAL: tactic_expr;
-  ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
-  tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
+  GLOBAL: ltac_expr;
+  ssrparentacarg: [[ "("; tac = ltac_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
+  ltac_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
 END
 
 (** The internal "done" and "ssrautoprop" tactics. *)
@@ -1741,7 +1741,7 @@ let tclBY tac = Tacticals.New.tclTHEN tac (donetac ~-1)
 (* The latter two are used in forward-chaining tactics (have, suffice, wlog) *)
 (* and subgoal reordering tacticals (; first & ; last), respectively.        *)
 
-(* Force use of the tactic_expr parsing entry, to rule out tick marks. *)
+(* Force use of the ltac_expr parsing entry, to rule out tick marks. *)
 
 (** The "by" tactical. *)
 
@@ -1782,12 +1782,12 @@ let ssrdotac_expr ?loc n m tac clauses =
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: tactic_expr;
+  GLOBAL: ltac_expr;
   ssrdotac: [
-    [ tac = tactic_expr LEVEL "3" -> { mk_hint tac }
+    [ tac = ltac_expr LEVEL "3" -> { mk_hint tac }
     | tacs = ssrortacarg -> { tacs }
   ] ];
-  tactic_expr: LEVEL "3" [ RIGHTA
+  ltac_expr: LEVEL "3" [ RIGHTA
     [ IDENT "do"; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses ->
       { ssrdotac_expr ~loc noindex m tac clauses }
     | IDENT "do"; tac = ssrortacarg; clauses = ssrclauses ->
@@ -1833,20 +1833,20 @@ let tclseq_expr ?loc tac dir arg =
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: tactic_expr;
+  GLOBAL: ltac_expr;
   ssr_first: [
     [ tac = ssr_first; ipats = ssrintros_ne -> { tclintros_expr ~loc tac ipats }
-    | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> { TacFirst tacl }
+    | "["; tacl = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst tacl }
     ] ];
   ssr_first_else: [
     [ tac1 = ssr_first; tac2 = ssrorelse -> { TacOrelse (tac1, tac2) }
     | tac = ssr_first -> { tac } ]];
-  tactic_expr: LEVEL "4" [ LEFTA
-    [ tac1 = tactic_expr; ";"; IDENT "first"; tac2 = ssr_first_else ->
+  ltac_expr: LEVEL "4" [ LEFTA
+    [ tac1 = ltac_expr; ";"; IDENT "first"; tac2 = ssr_first_else ->
       { TacThen (tac1, tac2) }
-    | tac = tactic_expr; ";"; IDENT "first"; arg = ssrseqarg ->
+    | tac = ltac_expr; ";"; IDENT "first"; arg = ssrseqarg ->
       { tclseq_expr ~loc tac L2R arg }
-    | tac = tactic_expr; ";"; IDENT "last"; arg = ssrseqarg ->
+    | tac = ltac_expr; ";"; IDENT "last"; arg = ssrseqarg ->
       { tclseq_expr ~loc tac R2L arg }
     ] ];
 END
@@ -2447,8 +2447,8 @@ END
 
 (* The standard TACTIC EXTEND does not work for abstract *)
 GRAMMAR EXTEND Gram
-  GLOBAL: tactic_expr;
-  tactic_expr: LEVEL "3"
+  GLOBAL: ltac_expr;
+  ltac_expr: LEVEL "3"
     [ RIGHTA [ IDENT "abstract"; gens = ssrdgens ->
                { ssrtac_expr ~loc "abstract"
                 [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]];
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 91cd5b251c..a49a5e8b28 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -85,7 +85,7 @@ let mk_pat c (na, t) = (c, na, t)
 
 GRAMMAR EXTEND Gram
   GLOBAL: binder_constr;
-  ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> { mk_rtype t } ]];
+  ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]];
   ssr_mpat: [[ p = pattern -> { [[p]] } ]];
   ssr_dpat: [
     [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt }
@@ -96,9 +96,9 @@ GRAMMAR EXTEND Gram
   ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]];
   ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]];
   binder_constr: [
-    [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
+    [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
       { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
-    | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
+    | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
       { let b1, ct, rt = db1 in
       let b1, b2 = let open CAst in
         let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
@@ -119,7 +119,7 @@ END
 GRAMMAR EXTEND Gram
   GLOBAL: closed_binder;
   closed_binder: [
-    [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" ->
+    [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" ->
       { [CLocalAssum ([CAst.make ~loc Anonymous], Default Explicit, c)] }
   ] ];
 END
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 }