diff options
Diffstat (limited to 'proofs/tactic_debug.ml')
| -rw-r--r-- | proofs/tactic_debug.ml | 9 |
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 |