From d8e87360b6413d9eb02c2c47441c8f48b816eac3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 14 Oct 2016 19:06:10 +0200
Subject: Using "simple apply" and "simple eapply" in the trace of auto.

This is more precise and probably clearer (see e.g. thread
"Understanding auto" on coq-club).
---
 tactics/hints.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index d1343f296e..89ecc6c0b2 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1297,11 +1297,11 @@ let make_db_list dbnames =
 let pr_hint_elt (c, _, _) = pr_constr c
 
 let pr_hint h = match h.obj with
-  | Res_pf (c, _) -> (str"apply " ++ pr_hint_elt c)
-  | ERes_pf (c, _) -> (str"eapply " ++ pr_hint_elt c)
+  | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
+  | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt c)
   | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c)
   | Res_pf_THEN_trivial_fail (c, _) ->
-      (str"apply " ++ pr_hint_elt c ++ str" ; trivial")
+      (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial")
   | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
   | Extern tac ->
       let env =
-- 
cgit v1.2.3


From a40451fbd096703d9a06795c9294d11dfd7a74dd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 14 Oct 2016 19:59:46 +0200
Subject: Fixing English typography for colon.

---
 tactics/auto.ml  | 8 ++++----
 tactics/eauto.ml | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6d1a1ae28f..a6dc64b4e4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -269,10 +269,10 @@ let pr_info_nop = function
 
 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 : *)"
+  | (Debug,0,_) -> str "(* debug trivial: *)"
+  | (Debug,_,_) -> str "(* debug auto: *)"
+  | (Info,0,_) -> str "(* info trivial: *)"
+  | (Info,_,_) -> str "(* info auto: *)"
 
 let tclTRY_dbg d tac =
   let (level, _, _) = d in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 90f80a7377..c6d2448679 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -351,8 +351,8 @@ let pr_info_nop = function
 
 let pr_dbg_header = function
   | Off -> ()
-  | Debug -> Feedback.msg_debug (str "(* debug eauto : *)")
-  | Info  -> Feedback.msg_debug (str "(* info eauto : *)")
+  | Debug -> Feedback.msg_debug (str "(* debug eauto: *)")
+  | Info  -> Feedback.msg_debug (str "(* info eauto: *)")
 
 let pr_info dbg s =
   if dbg != Info then ()
-- 
cgit v1.2.3


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(-)

(limited to 'tactics')

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 7c047370dc9032e3ded3365a45de5b92e7c9033f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 14 Oct 2016 22:12:53 +0200
Subject: Fix bug #5139: Anomalies should not be caught by || / try.

There was a catch-all clause in the tclORELSE0 function. We now only
catch noncritical exceptions.
---
 tactics/tacticals.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 87fdcf14d4..66da9ee182 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -322,7 +322,7 @@ module New = struct
     try
       Refiner.catch_failerror e;
       tclUNIT ()
-    with e -> tclZERO e
+    with e when CErrors.noncritical e -> tclZERO e
 
   (* spiwack: I chose to give the Ltac + the same semantics as
      [Proofview.tclOR], however, for consistency with the or-else
-- 
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(-)

(limited to 'tactics')

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(-)

(limited to 'tactics')

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