From 80c41b77ab0d4ec24f489aa363b8bf78f6ee3143 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 6 Jan 2003 15:31:33 +0000
Subject: doc SearchAbout

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8304 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-oth.tex | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index c5bd636615..151cf51dcb 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}
-- 
cgit v1.2.3