From ec878d596f15ad2baa10395fffd3849df5597f78 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 15 Oct 2016 00:24:20 +0200
Subject: One more little bug in the output of "debug auto".

Header was missing in last commit.

One day, it would be nice to unify the display of "debug auto" and
"debug eauto"...
---
 tactics/auto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 65294dada..985650e49 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
-- 
cgit v1.2.3