Merge PR #12599: Remove the Refiner module

Reviewed-by: ejgallego

6 files changed, 10 insertions, 10 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/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f16d0717df..40dea90c00 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1567,7 +1567,7 @@ let assert_replacing id newt tac =
 
 let newfail n s =
   let info = Exninfo.reify () in
-  Proofview.tclZERO ~info (Refiner.FailError (n, lazy s))
+  Proofview.tclZERO ~info (Tacticals.FailError (n, lazy s))
 
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
@@ -1656,7 +1656,7 @@ let cl_rewrite_clause_strat progress strat clause =
       (fun (e, info) -> match e with
        | RewriteFailure e ->
          tclZEROMSG ~info (str"setoid rewrite failed: " ++ e)
-       | Refiner.FailError (n, pp) ->
+       | Tacticals.FailError (n, pp) ->
          tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp)
        | e ->
          Proofview.tclZERO ~info e))
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 705a1a62ce..fdebe14a23 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -22,7 +22,6 @@ open Util
 open Names
 open Nameops
 open Libnames
-open Refiner
 open Tacmach.New
 open Tactic_debug
 open Constrexpr
@@ -1103,8 +1102,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac)
   | TacShowHyps tac ->
          Proofview.V82.tactic begin
-           tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
-         end [@ocaml.warning "-3"]
+           Tacticals.tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
+         end
   | TacAbstract (t,ido) ->
       let call = LtacMLCall tac in
       let trace = push_trace(None,call) ist in
@@ -1442,6 +1441,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
     if the left-hand side fails. *)
 and interp_match_successes lz ist s =
    let general =
+     let open Tacticals in
      let break (e, info) = match e with
        | FailError (0, _) -> None
        | FailError (n, s) -> Some (FailError (pred n, s), info)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e7c75e029e..878f7a834e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -201,7 +201,7 @@ let exec_tactic env evd n f args =
   (* Evaluate the whole result *)
   let gl = dummy_goal env evd in
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
-  let evd = Evd.minimize_universes (Refiner.project gls) in
+  let evd = Evd.minimize_universes gls.Evd.sigma in
   let nf c = constr_of evd c in
   Array.map nf !tactic_res, Evd.universe_context_set evd
 
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 01e8daf82d..5f463f8de4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -748,7 +748,7 @@ let pf_abs_cterm gl n c0 = abs_cterm (pf_env gl) (project gl) n c0
 (* }}} *)
 
 let pf_merge_uc uc gl =
-  re_sig (sig_it gl) (Evd.merge_universe_context (Refiner.project gl) uc)
+  re_sig (sig_it gl) (Evd.merge_universe_context gl.Evd.sigma uc)
 let pf_merge_uc_of sigma gl =
   let ucst = Evd.evar_universe_context sigma in
   pf_merge_uc ucst gl
@@ -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 =