Deprecate the legacy tacticals from module Refiner.

5 files changed, 45 insertions, 12 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 0e7d3c2f3b..af53f16e1f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -395,7 +395,8 @@ let jmeq_refl () =
   with e when CErrors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
-  tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l
+  Proofview.V82.of_tactic
+    (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l)
 
 let h_id = Id.of_string "h"
 let hrec_id = Id.of_string "hrec"
@@ -428,15 +429,15 @@ let evaluable_of_global_reference r =
 
 let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) =
   let open Tacticals in
-  tclREPEAT
-    (List.fold_right
-       (fun (eq, b) i ->
-         tclORELSE
-           (Proofview.V82.of_tactic
-              ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
-           i)
-       (if rev then List.rev eqs else eqs)
-       (tclFAIL 0 (mt ())))
+  (tclREPEAT
+     (List.fold_right
+        (fun (eq, b) i ->
+          tclORELSE
+            (Proofview.V82.of_tactic
+               ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
+            i)
+        (if rev then List.rev eqs else eqs)
+        (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"])
 
 let decompose_lam_n sigma n =
   if n < 0 then
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index dda7f0742c..a8bb97c774 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1087,7 +1087,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacShowHyps tac ->
          Proofview.V82.tactic begin
            tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
-         end
+         end [@ocaml.warning "-3"]
   | TacAbstract (t,ido) ->
       let call = LtacMLCall tac in
       let trace = push_trace(None,call) ist in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e05c4c26dd..e8257b5dba 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -22,7 +22,7 @@ open Locusops
 
 open Ltac_plugin
 open Tacmach
-open Refiner
+open Tacticals
 open Libnames
 open Ssrmatching_plugin
 open Ssrmatching
@@ -81,6 +81,9 @@ let nohint = false, []
 
 type 'a tac_a = (goal * 'a) sigma -> (goal * 'a) list sigma
 
+let project gl = gl.Evd.sigma
+let re_sig it sigma = { Evd.it = it; Evd.sigma = sigma }
+
 let push_ctx  a gl = re_sig (sig_it gl, a) (project gl)
 let push_ctxs a gl =
   re_sig (List.map (fun x -> x,a) (sig_it gl)) (project gl)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 3471f38e9e..a3cbfb5d5d 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -28,42 +28,53 @@ val refiner : check:bool -> Constr.t -> unit Proofview.tactic
 
 (** [tclIDTAC] is the identity tactic without message printing*)
 val tclIDTAC          : tactic
+[@@ocaml.deprecated "Use Tactical.New.tclIDTAC"]
 val tclIDTAC_MESSAGE  : Pp.t -> tactic
+[@@ocaml.deprecated]
 
 (** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
+[@@ocaml.deprecated "Use Proofview.Unsafe.tclEVARS"]
 
 
 (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
 val tclTHEN          : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHEN"]
 
 (** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More
    convenient than [tclTHEN] when [n] is large *)
 val tclTHENLIST      : tactic list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENLIST"]
 
 (** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclMAP"]
 
 (** [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [(tac2 i)] to the [i]{^ th} resulting subgoal (starting from 1) *)
 val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHEN_i"]
 
 (** [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
    to the last resulting subgoal (previously called [tclTHENL]) *)
 val tclTHENLAST         : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENLAST"]
 
 (** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
    to the first resulting subgoal *)
 val tclTHENFIRST         : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENFIRST"]
 
 (** [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to
    [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
    an error if the number of resulting subgoals is not [n] *)
 val tclTHENSV         : tactic -> tactic array -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENSV"]
 
 (** Same with a list of tactics *)
 val tclTHENS         : tactic -> tactic list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENS"]
 
 (** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
@@ -71,15 +82,18 @@ val tclTHENS         : tactic -> tactic list -> tactic
    subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
    error if the number of resulting subgoals is strictly less than [n+m] *)
 val tclTHENS3PARTS     : tactic -> tactic array -> tactic -> tactic array -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENS3PARTS"]
 
 (** [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
    last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
 val tclTHENSLASTn     : tactic -> tactic -> tactic array -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENSLASTn"]
 
 (** [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then
    applies [t1],...,[tn] on the first [n] resulting subgoals and
    [tac2] for the remaining last subgoals (previously called tclTHENST) *)
 val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENSFIRSTn"]
 
 (** A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.t Lazy.t
@@ -89,15 +103,28 @@ exception FailError of int * Pp.t Lazy.t
 val catch_failerror  : Exninfo.iexn -> unit
 
 val tclORELSE0       : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclORELSE0"]
 val tclORELSE        : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclORELSE"]
 val tclREPEAT        : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclREPEAT"]
 val tclFIRST         : tactic list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclFIRST"]
 val tclTRY           : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTRY"]
 val tclTHENTRY       : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENTRY"]
 val tclCOMPLETE      : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclCOMPLETE"]
 val tclAT_LEAST_ONCE : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclAT_LEAST_ONCE"]
 val tclFAIL          : int -> Pp.t -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclFAIL"]
 val tclFAIL_lazy     : int -> Pp.t Lazy.t -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclFAIL_lazy"]
 val tclDO            : int -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclDO"]
 val tclPROGRESS      : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclPROGRESS"]
 val tclSHOWHYPS      : tactic -> tactic
+[@@ocaml.deprecated "Internal tactic. Do not use."]
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 07f9def2c8..374706c8f9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -29,6 +29,8 @@ module NamedDecl = Context.Named.Declaration
 
 type tactic = Proofview.V82.tac
 
+[@@@ocaml.warning "-3"]
+
 let tclIDTAC         = Refiner.tclIDTAC
 let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE
 let tclORELSE0       = Refiner.tclORELSE0