From 50edb9bb8d43b190996d1d85a2bfd95f52b2db19 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 11:28:19 +0100
Subject: [info_auto] & [info_trivial]: warning message to help users find
 [Info].

---
 tactics/tacinterp.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e4558481bc..af541b8b9e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1973,6 +1973,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
+      begin if debug == Tacexpr.Info then
+          msg_warning
+	    (strbrk"The \"info_trivial\" tactic" ++ spc ()
+           ++strbrk"does not print traces anymore." ++ spc()
+           ++strbrk"Use \"Info 1 trivial\", instead.")
+      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
@@ -1984,6 +1990,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	     (Option.map (List.map (interp_hint_base ist)) l))
       end
   | TacAuto (debug,n,lems,l) ->
+      begin if debug == Tacexpr.Info then
+          msg_warning
+	    (strbrk"The \"info_auto\" tactic" ++ spc ()
+           ++strbrk"does not print traces anymore." ++ spc()
+           ++strbrk"Use \"Info 1 auto\", instead.")
+      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-- 
cgit v1.2.3