doc SearchAbout

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8304 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 2 deletions

diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index c5bd63661..151cf51dc 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -148,8 +148,17 @@ library lemmas.
 \begin{ErrMsgs}
 \item \errindex{The reference \qualid\ was not found in the current
 environment}\\
-    There is no constant in the environment named
-    \qualid.
+    There is no constant in the environment named \qualid.
+\end{ErrMsgs}
+
+\subsection{\tt SearchAbout {\qualid}.}\comindex{SearchAbout}
+This command displays the name and type of all theorems of the current
+context whose statement contains \qualid.  This command is useful to
+remind the user of the name of library lemmas.
+\begin{ErrMsgs}
+\item \errindex{The reference \qualid\ was not found in the current
+environment}\\
+    There is no constant in the environment named \qualid.
 \end{ErrMsgs}
 
 \subsection{\tt SearchPattern {\term}.}\comindex{SearchPattern}