diff options
Diffstat (limited to 'proofs/tactic_debug.ml')
| -rw-r--r-- | proofs/tactic_debug.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 = |