Wrap the legacy refiner type into the Logic API.

4 files changed, 13 insertions, 17 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 695e103082..c5e341c720 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -13,7 +13,6 @@ open Constr
 open Termops
 open Evd
 open EConstr
-open Refiner
 open Logic
 open Reduction
 open Clenv
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 4eb8658f83..b12d966387 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -581,10 +581,19 @@ let prim_refiner r sigma goal =
   let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in
   let sgl = List.rev sgl in
   let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
-  (sgl, sigma)
+  { Evd.it = sgl; Evd.sigma = sigma; }
 
-let prim_refiner ~check r sigma goal =
+let refiner ~check r { Evd.sigma = sigma; Evd.it = goal } =
   if check then
     with_check (prim_refiner r sigma) goal
   else
     prim_refiner r sigma goal
+
+(* Profiling refiner *)
+let refiner ~check =
+  if Flags.profile then
+    let refiner_key = CProfile.declare_profile "refiner" in
+      CProfile.profile2 refiner_key (refiner ~check)
+  else refiner ~check
+
+let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 5d21474394..e4fed22860 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -26,7 +26,7 @@ open Evd
 
 (** The primitive refiner. *)
 
-val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map
+val refiner : check:bool -> constr -> unit Proofview.tactic
 
 (** {6 Refiner errors. } *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 29a47c5acd..874bab277d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -12,7 +12,6 @@ open Pp
 open CErrors
 open Util
 open Evd
-open Logic
 
 type tactic = Proofview.V82.tac
 
@@ -26,18 +25,7 @@ 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 ~check pr goal_sigma =
-  let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in
-  { it = sgl; sigma = sigma'; }
-
-(* Profiling refiner *)
-let refiner ~check =
-  if Flags.profile then
-    let refiner_key = CProfile.declare_profile "refiner" in
-      CProfile.profile2 refiner_key (refiner ~check)
-  else refiner ~check
-
-let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c)
+let refiner = Logic.refiner
 
 (*********************)
 (*   Tacticals       *)