Merge branch 'v8.6'

4 files changed, 18 insertions, 24 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index c66fad651..63f85114e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -259,31 +259,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 ()
+      Feedback.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,_,_) -> Feedback.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,_) -> Feedback.msg_debug (str "(* debug trivial: *)")
+  | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)")
+  | (Info,0,_) -> Feedback.msg_debug (str "(* info trivial: *)")
+  | (Info,_,_) -> Feedback.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
-  | Off -> tac
-  | Debug | Info -> delay (fun () -> Feedback.msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac)
-  in
-  let after = match level with
-  | Info -> delay (fun () -> Feedback.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
 
 (**************************************************************************)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index e9e00f201..c6b7de32d 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 ()
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7dc40079e..3d5be5441 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1299,11 +1299,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 =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f739488aa..93c04e373 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -324,7 +324,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