Backporting 11445 from 8.2 to trunk (negative conditions in

SearchAbout + referring objects by their notation).



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

1 files changed, 26 insertions, 6 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index ec07dc079c..7c6bf7297c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -135,14 +135,34 @@ environment}\\
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{}
+\item {\tt SearchAbout {\str}.}
+
+If {\str} is a valid identifier, this command displays the name and type
+of all objects (theorems, axioms, etc) of the current context whose
+name contains {\str}. If {\str} is a notation's string denoting some
+reference {\qualid} (referred to by its main symbol as in \verb="+"=
+or by its notation's string as in \verb="_ + _"= or \verb="_ 'U' _"=, see
+Section~\ref{Notation}), the command works like {\tt SearchAbout
+{\qualid}}.
+
+\item {\tt SearchAbout {\str}\%{\delimkey}.}
+
+The string {\str} must be a notation or the main symbol of a notation
+which is then interpreted in the scope bound to the delimiting key
+{\delimkey} (see Section~\ref{scopechange}).
+
+\item {\tt SearchAbout [ \nelist{\zeroone{-}\textrm{\textsl{qualid-or-string}}}{}
 ].}\\
 \noindent where {\textrm{\textsl{qualid-or-string}}} is a {\qualid} or
-a {\str}.
-
-This extension of {\tt SearchAbout} searches for all objects whose
-statement mentions all of {\qualid} of the list and whose name
-contains all {\str} of the list.
+a {\str}, or a {\str} followed by a scope delimiting key 
+{\tt \%{\delimkey}}.
+
+This generalization of {\tt SearchAbout} searches for all objects
+whose statement mentions all of {\qualid} (or {\str} if {\str} is the
+notation for a reference) and whose name contains all {\str} that
+correspond to valid identifiers. If a {\qualid} or a {\str} is
+prefixed by ``-'', the search excludes the objects that mention that
+{\qualid} or that {\str}.
 
 \Example