Fix Bug 3131 + Really drop mentions of info in refman.

2 files changed, 2 insertions, 11 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 267226f3b7..9f65c0ef03 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -68,7 +68,7 @@ form {\tt ltac :} {\qualid}. To force the resolution as a reference to
 a term, use the syntax {\tt ({\qualid})}.
 
 \item As shown by the figure, tactical {\tt ||} binds more than the
-prefix tacticals {\tt try}, {\tt repeat}, {\tt do}, {\tt info} and
+prefix tacticals {\tt try}, {\tt repeat}, {\tt do} and
 {\tt abstract} which themselves bind more than the postfix tactical
 ``{\tt \dots\ ;[ \dots\ ]}'' which binds more than ``\dots\ {\tt ;}
 \dots''.
@@ -96,7 +96,6 @@ is understood as
 \\
 {\tacexprpref} & ::= &
            {\tt do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
-& | & {\tt info} {\tacexprpref}\\
 & | & {\tt progress} {\tacexprpref}\\
 & | & {\tt repeat} {\tacexprpref}\\
 & | & {\tt try} {\tacexprpref}\\
@@ -839,14 +838,6 @@ The following returns the type of {\term}:
 {\tt type of} {\term}
 \end{quote}
 
-\subsubsection[Accessing tactic decomposition]{Accessing tactic decomposition\tacindex{info}
-\index{Tacticals!info@{\tt info}}}
-
-Tactical ``{\tt info} {\tacexpr}'' is not really a tactical. For
-elementary tactics, this is equivalent to \tacexpr. For complex tactic
-like \texttt{auto}, it displays the operations performed by the
-tactic.
-
 \subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}
 \index{Tacticals!abstract@{\tt abstract}}}
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index e318446a42..89d8df473b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3589,7 +3589,7 @@ Hint Extern 5   ({?X1 = ?X2} + {?X1 <> ?X2}) =>
  generalize X1, X2; decide equality : eqdec.
 Goal
 forall a b:list (nat * nat), {a = b} + {a <> b}.
-info auto with eqdec.
+info_auto with eqdec.
 \end{coq_example}
 \begin{coq_eval}
 Abort.