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

3 files changed, 36 insertions, 9 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
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 22eb0eeaec..967a8180ad 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -713,13 +713,13 @@ ways to change the interpretation of subterms are available.
 \comindex{Delimit Scope}}
 
 It is possible to locally extend the interpretation scope stack using
-the syntax ({\term})\%{\nterm{key}} (or simply {\term}\%{\nterm{key}}
-for atomic terms), where {\nterm{key}} is a special identifier called
+the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey}
+for atomic terms), where {\delimkey} is a special identifier called
 {\em delimiting key} and bound to a given scope.
 
 In such a situation, the term {\term}, and all its subterms, are
 interpreted in the scope stack extended with the scope bound to
-{\nterm{key}}.
+{\delimkey}.
 
 To bind a delimiting key to a scope, use the command
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index bb845beb17..ca06e1d782 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1317,6 +1317,13 @@ with its $\beta\iota$-normal form.
   this notation refers to an unfoldable constant, then the tactic
   unfolds it.
 
+\item {\tt unfold {\qstring}\%{\delimkey}}
+
+  This is variant of {\tt unfold {\qstring}} where {\qstring} gets its
+  interpretation from the scope bound to the delimiting key
+  {\delimkey} instead of its default interpretation (see
+  Section~\ref{scopechange}).
+
 \item {\tt unfold \qualidorstring$_1$ at \num$_1^1$, \dots, \num$_i^1$,
 \dots,\ \qualidorstring$_n$ at \num$_1^n$ \dots\ \num$_j^n$}