From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- proofs/tactic_debug.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'proofs/tactic_debug.ml') diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index b56cb844..27ab990c 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -140,11 +140,11 @@ let debug_prompt lev g tac f = else (decr skip; run false; if !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 - ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e); - raise e + if Logic.catchable_exception reraise then + ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error reraise); + raise reraise (* Prints a constr *) let db_constr debug env c = -- cgit v1.2.3