diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
commit | e347929583f820a2cc0296597b6382309e930989 (patch) | |
tree | cdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /tactics/tacticals.ml | |
parent | c01be74d81a5466c58f8dc6c568db286b0979997 (diff) | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 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 |