Remove Refiner.refiner.

7 files changed, 7 insertions, 11 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2151ad7873..9b578d4697 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -43,7 +43,7 @@ let finish_proof dynamic_infos g =
 
 let refine c =
   Proofview.V82.of_tactic
-    (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c))
+    (Logic.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 01e8daf82d..5c25db1a82 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1029,7 +1029,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t =
     pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
     Proofview.(V82.of_tactic
       (Tacticals.New.tclTHENLIST [
-         Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t);
+         Logic.refiner ~check:false EConstr.Unsafe.(to_constr t);
          (if first_goes_last then cycle 1 else tclUNIT ())
       ])) gl
   end
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 8e75ba7a2b..a12b4aad11 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -482,7 +482,7 @@ let revtoptac n0 =
   let dc, cl = EConstr.decompose_prod_n_assum sigma n concl 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 ()|])))
+  Logic.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])))
   end
 
 let equality_inj l b id c =
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3c6a5d1694..8e413c7a88 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -21,8 +21,6 @@ let project x = x.sigma
 let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
 let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
 
-let refiner = Logic.refiner
-
 (* A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.t Lazy.t
 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 0ea630fdbc..18ac5f4a76 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -22,8 +22,6 @@ 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 -> unit Proofview.tactic
-
 (** A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.t Lazy.t
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 39017c946f..3aa7626aaa 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1047,7 +1047,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 = Clenv.clenv_value_cast_meta absurd_clause in
     tclTHENS (assert_after Anonymous false_0)
-      [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]
+      [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))]
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
@@ -1366,7 +1366,7 @@ 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 ->
-           Refiner.refiner ~check:true EConstr.Unsafe.(to_constr
+           Logic.refiner ~check:true EConstr.Unsafe.(to_constr
              (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
           ])]
   with Exit ->
@@ -1412,7 +1412,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;
-            Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)])
+            Logic.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 3133f9be1e..eb7f2190a8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1383,7 +1383,7 @@ let clenv_refine_in ?err 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 = Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in
+  let exact_tac = Logic.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