diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
| commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
| tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /proofs/tactic_debug.ml | |
| parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) | |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
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 = |