Merge PR #12227: Spring cleaning of the tactic compatibility layer

Reviewed-by: gares

4 files changed, 10 insertions, 6 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f3073acb0a..e1d34af13e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1043,7 +1043,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
     let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
     let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
     tclTHENS (assert_after Anonymous false_0)
-      [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))]
+      [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
@@ -1360,8 +1360,8 @@ let inject_if_homogenous_dependent_pair ty =
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
           [clear [destVar sigma hyp];
            Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 ->
-           Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr
-             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
+           Refiner.refiner ~check:true EConstr.Unsafe.(to_constr
+             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
           ])]
   with Exit ->
     Proofview.tclUNIT ()
@@ -1406,7 +1406,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       (Proofview.tclIGNORE (Proofview.Monad.List.map
          (fun (pf,ty) -> tclTHENS (cut ty)
            [inject_if_homogenous_dependent_pair ty;
-            Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))])
+            Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)])
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 8f6844079b..07f9def2c8 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -368,6 +368,9 @@ module New = struct
     Proofview.Unsafe.tclNEWGOALS tl <*>
     Proofview.tclUNIT ans
 
+  let tclTHENSLASTn t1 repeat l =
+    tclTHENS3PARTS t1 [||] repeat l
+
   let tclTHENLASTn t1 l =
     tclTHENS3PARTS t1 [||] (tclUNIT()) l
   let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 9ec558f1ad..01565169ca 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -180,6 +180,7 @@ module New : sig
       middle. Raises an error if the number of resulting subgoals is
       strictly less than [n+m] *)
   val tclTHENS3PARTS     : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic
+  val tclTHENSLASTn    : unit tactic -> unit tactic -> unit tactic array -> unit tactic
   val tclTHENSFIRSTn : unit tactic -> unit tactic array -> unit tactic -> unit tactic
   val tclTHENFIRSTn : unit tactic -> unit tactic array -> unit tactic
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0df4f5b207..e4809332c5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1368,7 +1368,7 @@ let clenv_refine_in with_evars targetid id sigma0 clenv tac =
   if not with_evars && occur_meta clenv.evd new_hyp_typ then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
-  let exact_tac = Proofview.V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf)) in
+  let exact_tac = Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in
   let naming = NamingMustBe (CAst.make targetid) in
   let with_clear = do_replace (Some id) naming in
   Tacticals.New.tclTHEN
@@ -1670,7 +1670,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
             | Some (p,pt) ->
               Tacticals.New.tclTHENS
                 (assert_before_gen false (NamingAvoid avoid) pt)
-                [Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p));
+                [refiner ~check:true EConstr.Unsafe.(to_constr p);
                  (* Might be ill-typed due to forbidden elimination. *)
                  Tacticals.New.onLastHypId (tac (not isrec))]
            end)))