From 58d1381316560eadbe859b53780fe8da7723ad31 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 14 Oct 2016 20:03:23 +0200
Subject: Fixing printing of info_auto broken since 0091c528 (2014).

---
 tactics/auto.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 45da04cf00..65294dadad 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -272,8 +272,8 @@ let tclTRY_dbg d tac =
   let (level, _, _) = d in
   let delay f = Proofview.tclUNIT () >>= fun () -> f () in
   let tac = match level with
-  | Off -> tac
-  | Debug | Info -> delay (fun () -> msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac)
+  | Debug | Off -> 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
   | Info -> delay (fun () -> msg_debug (pr_info_nop d); Proofview.tclUNIT ())
-- 
cgit v1.2.3