From 924771d6fdd1349955c2d0f500ccf34c2109507b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 17 Aug 2014 19:26:58 +0200 Subject: Improving error message when applying rewrite to an expression which is not an equality. --- proofs/refiner.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'proofs') 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 *) -- cgit v1.2.3