aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 632f83c83..152556c74 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