Merge remote-tracking branch 'github/pr/338' into v8.5

Was PR#338: Remove warning now that info_auto is fixed.

Author: maximedenes

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