diff options
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 75c3436cf4..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,16 +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 = Logic.refiner (*********************) (* Tacticals *) @@ -269,5 +259,3 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} -let tclPUSHEVARUNIVCONTEXT ctx gl = - tclEVARS (Evd.merge_universe_context (project gl) ctx) gl |