diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 00:00:40 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 00:00:40 +0000 |
| commit | 1b2e9b8aa5b5b0941ac331c1a95b406c053ffbdf (patch) | |
| tree | 59a175569af4ac1e3a593a8163b695931affb497 /proofs/refiner.ml | |
| parent | 7e50cbcc7e0ecbc9c4dd7bace9f2cb261a2c2d84 (diff) | |
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
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 = |