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

1 files changed, 5 insertions, 4 deletions

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