From 674f353d32ec2dc957a2402e528290c4695e761b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 31 Oct 2014 11:10:04 +0100
Subject: Info: the warning message of the defunct [info] tactic now points to
 the [Info] command.

---
 tactics/tacinterp.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 10f382a9e5..d589f0c180 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1168,8 +1168,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacArg a -> interp_tactic ist (TacArg a)
   | TacInfo tac ->
       msg_warning
-	(strbrk "The general \"info\" tactic is currently not working." ++ fnl () ++
-	   strbrk "Some specific verbose tactics may exist instead, such as info_trivial, info_auto, info_eauto.");
+	(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.");
       eval_tactic ist tac
   (* For extensions *)
   | TacAlias (loc,s,l) ->
-- 
cgit v1.2.3