diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 68fdea652b..391a78b34a 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -272,11 +272,14 @@ let ite_gen tcal tac_if continue tac_else gl= if !success then raise e else - tac_else gl in - try - tcal tac_if0 continue gl - with (* Breakpoint *) - | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl + try + tac_else gl + with + e' when Errors.noncritical e' -> raise e in + try + tcal tac_if0 continue gl + with (* Breakpoint *) + | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl (* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) |