Rename tactic_expr -> ltac_expr

9 files changed, 59 insertions, 56 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 f8fbf0c2d0..affcf814d7 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -74,21 +74,21 @@ 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_arg command hint
           tactic_mode constr_may_eval constr_eval toplevel_selector
           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)) }
+    [ [ ta = ltac_expr; "|"; tg = tactic_then_gen -> { 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) }
+      | ta = ltac_expr -> { ([ta], None) }
       | "|"; tg = tactic_then_gen -> { 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 = tactic_then_gen; "]" -> {
           let (first,tail) = tg in
           match l , tail with
           | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
@@ -111,40 +111,40 @@ 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) } ]
+      | 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 } ];
@@ -154,7 +154,7 @@ GRAMMAR EXTEND Gram
       | r = reference; la = LIST0 tactic_arg_compat ->
         { TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ]
     | "0"
-      [ "("; a = tactic_expr; ")" -> { a }
+      [ "("; a = ltac_expr; ")" -> { a }
       | "["; ">"; tg = tactic_then_gen; "]" -> {
           let (tf,tail) = tg in
           begin match tail with
@@ -166,14 +166,14 @@ 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:
@@ -223,11 +223,11 @@ 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:
@@ -251,18 +251,18 @@ GRAMMAR EXTEND Gram
   ;
   match_context_rule:
     [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
-        "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
+        "=>"; te = ltac_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 } ] ]
+        "]"; "=>"; 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:
@@ -344,7 +344,7 @@ GRAMMAR EXTEND Gram
         { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
   ;
   term: LEVEL "0"
-    [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
+    [ [ 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 18fc9ce9d4..7b020c40ba 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -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..1631215d58 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -38,7 +38,8 @@ let clause_dft_concl =
 
 (* Main entries for ltac *)
 let tactic_arg = Entry.create "tactic_arg"
-let tactic_expr = Entry.create "tactic_expr"
+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..a2424d4c60 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -32,7 +32,9 @@ 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_arg : raw_tactic_arg Entry.t
+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..159ca678e9 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
 
 (**********************************************************************)
@@ -555,7 +555,7 @@ 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;
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. *)