From ebf4d8e58eeddaf5237447a9a0f21de48e72caa5 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 11:23:03 +0100
Subject: [info] tactical warning: do not suggest [info_auto] and
 [info_trivial].

Since they don't work anymore.
---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3b497faab5..e4558481bc 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1187,7 +1187,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       msg_warning
 	(strbrk "The general \"info\" tactic is currently not working." ++ spc()++
            strbrk "There is an \"Info\" command to replace it." ++fnl () ++
-	   strbrk "Some specific verbose tactics may also exist, such as info_trivial, info_auto, info_eauto.");
+	   strbrk "Some specific verbose tactics may also exist, such as info_eauto.");
       eval_tactic ist tac
   (* For extensions *)
   | TacAlias (loc,s,l) ->
-- 
cgit v1.2.3