Merge PR #12307: Cleaning up the legacy proof engine

Reviewed-by: ejgallego

1 files changed, 1 insertions, 13 deletions

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       *)