aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/auto.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 65294dadad..985650e49d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -272,7 +272,7 @@ let tclTRY_dbg d tac =
let (level, _, _) = d in
let delay f = Proofview.tclUNIT () >>= fun () -> f () in
let tac = match level with
- | Debug | Off -> tac
+ | Debug | Off -> delay (fun () -> msg_debug (pr_dbg_header d); tac)
| Info -> delay (fun () -> msg_debug (pr_dbg_header d); tac) >>= fun () -> msg_debug (pr_info_trace d); Proofview.tclUNIT ()
in
let after = match level with