From d2e713c3913c995ba3796863f778556e00cc5051 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 19 Oct 2016 18:30:44 +0200
Subject: Remove warning now that info_auto is fixed.

Removes a warning dating from 8.5 signaling that info_auto
and info_trivial are broken and advising to use Info 1 auto
instead. Now, these tactics are fixed and thus they can be
used again. They do not do exactly the same thing as
Info 1 auto and may be more useful for the learner.
---
 tactics/tacinterp.ml | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c3f7fa1439..23d188aa73 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2023,12 +2023,6 @@ 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
@@ -2039,13 +2033,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	     lems
 	     (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