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/tactic_debug.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'proofs/tactic_debug.ml')

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 5952fd29cb..8ad92910f3 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -142,11 +142,12 @@ let debug_prompt lev g tac f =
     else (decr skip; run false; if Int.equal !skip 0 then skipped:=0; DebugOn (lev+1)) in
   (* What to execute *)
   try f newlevel
-  with e ->
+  with reraise ->
     skip:=0; skipped:=0;
-    if Logic.catchable_exception e then
-      msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
-    raise e
+    if Logic.catchable_exception reraise then
+      msg_tac_debug
+        (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error reraise);
+    raise reraise
 
 let is_debug db = match db, !breakpoint with
 | DebugOff, _ -> false
-- 
cgit v1.2.3