Wrap Refiner.refiner in the tactic monad.

This function was used almost everywhere with the wrapper around.

8 files changed, 16 insertions, 11 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 7b2ce671a3..f4200854c2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -41,7 +41,10 @@ let observe_tac s = observe_tac (fun _ _ -> Pp.str s)
 let finish_proof dynamic_infos g =
   observe_tac "finish" (Proofview.V82.of_tactic assumption) g
 
-let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)
+let refine c =
+  Proofview.V82.of_tactic
+    (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c))
+
 let thin l = Proofview.V82.of_tactic (Tactics.clear l)
 let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v
 
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 134a9e4b36..95a0790ff3 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1014,7 +1014,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t g
     pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
     Proofview.(V82.of_tactic
       (Tacticals.New.tclTHENLIST [
-         V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t));
+         Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t);
          (if first_goes_last then cycle 1 else tclUNIT ())
       ])) gl
 
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index b44600a8cf..8f445b4397 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -477,7 +477,7 @@ let revtoptac n0 gl =
   let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in
   let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in
   let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in
-  Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl
+  Proofview.V82.of_tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])))) gl
 
 let equality_inj l b id c gl =
   let msg = ref "" in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 197d69a481..695e103082 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -77,7 +77,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
   let clenv = { clenv with evd = evd' } in
   Proofview.tclTHEN
     (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd'))
-    (Proofview.V82.tactic (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))))
+    (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))
   end
 
 let clenv_pose_dependent_evars ?(with_evars=false) clenv =
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 75c3436cf4..6a0ba30bbf 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -37,6 +37,8 @@ let refiner ~check =
       CProfile.profile2 refiner_key (refiner ~check)
   else refiner ~check
 
+let refiner ~check c = Proofview.V82.tactic (refiner ~check c)
+
 (*********************)
 (*   Tacticals       *)
 (*********************)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 66eae1db81..d4f2239a59 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -22,7 +22,7 @@ val project : 'a sigma -> evar_map
 val pf_env  : Goal.goal sigma -> Environ.env
 val pf_hyps : Goal.goal sigma -> named_context
 
-val refiner : check:bool -> Constr.t -> tactic
+val refiner : check:bool -> Constr.t -> unit Proofview.tactic
 
 (** {6 Tacticals. } *)
 
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/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)))