From 1b2e9b8aa5b5b0941ac331c1a95b406c053ffbdf Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 13 Mar 2013 00:00:40 +0000 Subject: Restrict (try...with...) to avoid catching critical exn (part 12) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16288 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/refiner.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'proofs/refiner.ml') diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 4592c60dd..04d125804 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -231,7 +231,7 @@ let tclORELSE0 t1 t2 g = try t1 g with (* Breakpoint *) - | e -> catch_failerror e; t2 g + | e when Errors.noncritical e -> catch_failerror e; t2 g (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) @@ -243,7 +243,7 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 let tclORELSE_THEN t1 t2then t2else gls = match try Some(tclPROGRESS t1 gls) - with e -> catch_failerror e; None + with e when Errors.noncritical e -> catch_failerror e; None with | None -> t2else gls | Some sgl -> @@ -274,7 +274,7 @@ let ite_gen tcal tac_if continue tac_else gl= try tcal tac_if0 continue gl with (* Breakpoint *) - | e -> catch_failerror e; tac_else0 e gl + | 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 *) @@ -328,7 +328,7 @@ let tclTIMEOUT n t g = | TacTimeout -> restore_timeout (); errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!") - | e -> restore_timeout (); raise e + | reraise -> restore_timeout (); raise reraise (* Beware: call by need of CAML, g is needed *) let rec tclREPEAT t g = -- cgit v1.2.3