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

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

9 files changed, 85 insertions, 82 deletions

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. *)