diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 24 |
1 files changed, 10 insertions, 14 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index cf2126f8..9b16fe3f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -16,7 +16,6 @@ open Context open Declarations open Tacmach open Clenv -open Misctypes (************************************************************************) (* Tacticals re-exported from the Refiner module *) @@ -494,26 +493,23 @@ module New = struct let (loc,_) = evi.Evd.evar_source in Pretype_errors.error_unsolvable_implicit loc env sigma evk None - let tclWITHHOLES accept_unresolved_holes tac sigma x = + let tclWITHHOLES accept_unresolved_holes tac sigma = tclEVARMAP >>= fun sigma_initial -> - if sigma == sigma_initial then tac x + if sigma == sigma_initial then tac else - let check_evars env new_sigma sigma initial_sigma = - try - check_evars env new_sigma sigma initial_sigma; - tclUNIT () - with e when Errors.noncritical e -> - tclZERO e - in - let check_evars_if = + let check_evars_if x = if not accept_unresolved_holes then tclEVARMAP >>= fun sigma_final -> tclENV >>= fun env -> - check_evars env sigma_final sigma sigma_initial + try + let () = check_evars env sigma_final sigma sigma_initial in + tclUNIT x + with e when Errors.noncritical e -> + tclZERO e else - tclUNIT () + tclUNIT x in - Proofview.Unsafe.tclEVARS sigma <*> tac x <*> check_evars_if + Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if let tclTIMEOUT n t = Proofview.tclOR |