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


From ec878d596f15ad2baa10395fffd3849df5597f78 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
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(-)

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
-- 
cgit v1.2.3


From e349809cf36289dc73249b2861007cc24e01bfa7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 15 Oct 2016 01:04:02 +0200
Subject: Still a problem with debug auto printing.

"msg_debug (mt())" is not identity, so we return back to how it was
done in 8.4, contracting a repeated pattern-matching into one.
---
 tactics/auto.ml | 30 ++++++++++++------------------
 1 file changed, 12 insertions(+), 18 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 985650e49d..fd25265e96 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -254,31 +254,25 @@ let pr_info_atom (d,pp) =
 
 let pr_info_trace = function
   | (Info,_,{contents=(d,Some pp)::l}) ->
-      prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)
-  | _ -> mt ()
+      msg_debug (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l))
+  | _ -> ()
 
 let pr_info_nop = function
-  | (Info,_,_) -> str "idtac."
-  | _ -> mt ()
+  | (Info,_,_) -> msg_debug (str "idtac.")
+  | _ -> ()
 
 let pr_dbg_header = function
-  | (Off,_,_) -> mt ()
-  | (Debug,0,_) -> str "(* debug trivial : *)"
-  | (Debug,_,_) -> str "(* debug auto : *)"
-  | (Info,0,_) -> str "(* info trivial : *)"
-  | (Info,_,_) -> str "(* info auto : *)"
+  | (Off,_,_) -> ()
+  | (Debug,0,_) -> msg_debug (str "(* debug trivial : *)")
+  | (Debug,_,_) -> msg_debug (str "(* debug auto : *)")
+  | (Info,0,_) -> msg_debug (str "(* info trivial : *)")
+  | (Info,_,_) -> msg_debug (str "(* info auto : *)")
 
 let tclTRY_dbg d tac =
-  let (level, _, _) = d in
   let delay f = Proofview.tclUNIT () >>= fun () -> f () in
-  let tac = match level with
-  | 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
-  | Info -> delay (fun () -> msg_debug (pr_info_nop d); Proofview.tclUNIT ())
-  | Off | Debug -> Proofview.tclUNIT ()
-  in
+  let tac = delay (fun () -> pr_dbg_header d; tac) >>=
+              fun () -> pr_info_trace d; Proofview.tclUNIT () in
+  let after = delay (fun () -> pr_info_nop d; Proofview.tclUNIT ()) in
   Tacticals.New.tclORELSE0 tac after
 
 (**************************************************************************)
-- 
cgit v1.2.3