diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
| commit | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch) | |
| tree | 12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /tactics/tacticals.ml | |
| parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) | |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
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 |