diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.mli | 1 | ||||
| -rw-r--r-- | proofs/refiner.ml | 10 |
2 files changed, 4 insertions, 7 deletions
diff --git a/proofs/logic.mli b/proofs/logic.mli index 5342b94b3e..ef8b2731b2 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -50,6 +50,7 @@ exception RefinerError of Environ.env * evar_map * refiner_error val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a val catchable_exception : exn -> bool +[@@ocaml.deprecated "This function does not scale in the presence of dynamically added exceptions. Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."] (** Move destination for hypothesis *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 2ef54540ff..75c3436cf4 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -204,14 +204,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) let catch_failerror (e, info) = - if catchable_exception e then Control.check_for_interrupt () - else match e with - | FailError (0,_) -> - Control.check_for_interrupt () - | FailError (lvl,s) -> + match e with + | FailError (lvl,s) when lvl > 0 -> Exninfo.iraise (FailError (lvl - 1, s), info) - | e -> Exninfo.iraise (e, info) - (** FIXME: do we need to add a [Errors.push] here? *) + | e -> Control.check_for_interrupt () (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) let tclORELSE0 t1 t2 g = |