diff options
| author | Hugo Herbelin | 2020-03-02 21:15:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-13 07:37:25 +0100 |
| commit | 89a5abb0b8b453bdda8c9ebf33734c42c3a826db (patch) | |
| tree | dc96f080513504f8b9609a18034c456453659caf /proofs | |
| parent | cd4253ee5db24873ea131554c80650ed6d5dbd13 (diff) | |
Removing catchable_exception test in tclOR/tclORELSE.
Since tclOR/tclORELSE are not supposed to return critical exceptions,
we don't need to replace catchable_exception by noncritical.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index fd73ab1b5a..825cd938fb 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 = |