diff options
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 13 |
1 files changed, 11 insertions, 2 deletions
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) |