diff options
| author | Pierre-Marie Pédrot | 2014-04-25 13:59:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-25 14:00:43 +0200 |
| commit | b35edb34769fecd4dbdf7030222ba3078eab1c93 (patch) | |
| tree | 0efb56c5711b0a2d9ae8eef5b7792b734899f2be /tactics/auto.ml | |
| parent | a5e0b28f9344744edf2209001fe047b1535775f6 (diff) | |
Fixing various backtrace recordings.
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 632f83c83a..152556c74a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1205,6 +1205,7 @@ let tclLOG (dbg,depth,trace) pp tac = msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); out with reraise -> + let reraise = Errors.push reraise in msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); raise reraise end @@ -1216,6 +1217,7 @@ let tclLOG (dbg,depth,trace) pp tac = trace := (depth, Some pp) :: !trace; out with reraise -> + let reraise = Errors.push reraise in trace := (depth, None) :: !trace; raise reraise end |