diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-17 19:26:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-18 18:56:39 +0200 |
| commit | 924771d6fdd1349955c2d0f500ccf34c2109507b (patch) | |
| tree | 1bb75c17f846a185c88bcd332e5890ebb2c41076 /proofs/refiner.ml | |
| parent | e8a531dfa623e3badc3baddcf13f0a7975c37886 (diff) | |
Improving error message when applying rewrite to an expression which is not an equality.
Diffstat (limited to 'proofs/refiner.ml')
| -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 68fdea652..391a78b34 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 *) |