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

4 files changed, 123 insertions, 95 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 69f9b2f410..be5980fe43 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -142,94 +142,95 @@
 \newcommand{\typecstr}{\zeroone{{\tt :} {\term}}}
 
 
-\newcommand{\Fwterm}{\textrm{\textsl{Fwterm}}}
-\newcommand{\Index}{\textrm{\textsl{index}}}
-\newcommand{\abbrev}{\textrm{\textsl{abbreviation}}}
-\newcommand{\atomictac}{\textrm{\textsl{atomic\_tactic}}}
-\newcommand{\bindinglist}{\textrm{\textsl{bindings\_list}}}
-\newcommand{\cast}{\textrm{\textsl{cast}}}
-\newcommand{\cofixpointbodies}{\textrm{\textsl{cofix\_bodies}}}
-\newcommand{\cofixpointbody}{\textrm{\textsl{cofix\_body}}}
-\newcommand{\commandtac}{\textrm{\textsl{tactic\_invocation}}}
-\newcommand{\constructor}{\textrm{\textsl{constructor}}}
-\newcommand{\convtactic}{\textrm{\textsl{conv\_tactic}}}
-\newcommand{\declarationkeyword}{\textrm{\textsl{declaration\_keyword}}}
-\newcommand{\declaration}{\textrm{\textsl{declaration}}}
-\newcommand{\definition}{\textrm{\textsl{definition}}}
-\newcommand{\digit}{\textrm{\textsl{digit}}}
-\newcommand{\exteqn}{\textrm{\textsl{ext\_eqn}}}
-\newcommand{\field}{\textrm{\textsl{field}}}
-\newcommand{\firstletter}{\textrm{\textsl{first\_letter}}}
-\newcommand{\fixpg}{\textrm{\textsl{fix\_pgm}}}
-\newcommand{\fixpointbodies}{\textrm{\textsl{fix\_bodies}}}
-\newcommand{\fixpointbody}{\textrm{\textsl{fix\_body}}}
-\newcommand{\fixpoint}{\textrm{\textsl{fixpoint}}}
-\newcommand{\flag}{\textrm{\textsl{flag}}}
-\newcommand{\form}{\textrm{\textsl{form}}}
-\newcommand{\entry}{\textrm{\textsl{entry}}} 
-\newcommand{\proditem}{\textrm{\textsl{production\_item}}} 
-\newcommand{\taclevel}{\textrm{\textsl{tactic\_level}}}
-\newcommand{\tacargtype}{\textrm{\textsl{tactic\_argument\_type}}} 
-\newcommand{\scope}{\textrm{\textsl{scope}}} 
-\newcommand{\optscope}{\textrm{\textsl{opt\_scope}}} 
-\newcommand{\declnotation}{\textrm{\textsl{decl\_notation}}} 
-\newcommand{\symbolentry}{\textrm{\textsl{symbol}}}
-\newcommand{\modifiers}{\textrm{\textsl{modifiers}}}
-\newcommand{\localdef}{\textrm{\textsl{local\_def}}}
-\newcommand{\localdecls}{\textrm{\textsl{local\_decls}}}
-\newcommand{\ident}{\textrm{\textsl{ident}}}
-\newcommand{\accessident}{\textrm{\textsl{access\_ident}}}
-\newcommand{\possiblybracketedident}{\textrm{\textsl{possibly\_bracketed\_ident}}}
-\newcommand{\inductivebody}{\textrm{\textsl{ind\_body}}}
-\newcommand{\inductive}{\textrm{\textsl{inductive}}}
-\newcommand{\naturalnumber}{\textrm{\textsl{natural}}}
-\newcommand{\integer}{\textrm{\textsl{integer}}}
-\newcommand{\multpattern}{\textrm{\textsl{mult\_pattern}}}
-\newcommand{\mutualcoinductive}{\textrm{\textsl{mutual\_coinductive}}}
-\newcommand{\mutualinductive}{\textrm{\textsl{mutual\_inductive}}}
-\newcommand{\nestedpattern}{\textrm{\textsl{nested\_pattern}}}
-\newcommand{\name}{\textrm{\textsl{name}}}
-\newcommand{\num}{\textrm{\textsl{num}}}
-\newcommand{\pattern}{\textrm{\textsl{pattern}}}
-\newcommand{\orpattern}{\textrm{\textsl{or\_pattern}}}
-\newcommand{\intropattern}{\textrm{\textsl{intro\_pattern}}}
-\newcommand{\disjconjintropattern}{\textrm{\textsl{disj\_conj\_intro\_pattern}}}
-\newcommand{\namingintropattern}{\textrm{\textsl{naming\_intro\_pattern}}}
-\newcommand{\pat}{\textrm{\textsl{pat}}}
-\newcommand{\pgs}{\textrm{\textsl{pgms}}}
-\newcommand{\pg}{\textrm{\textsl{pgm}}}
+\newcommand{\Fwterm}{\nterm{Fwterm}}
+\newcommand{\Index}{\nterm{index}}
+\newcommand{\abbrev}{\nterm{abbreviation}}
+\newcommand{\atomictac}{\nterm{atomic\_tactic}}
+\newcommand{\bindinglist}{\nterm{bindings\_list}}
+\newcommand{\cast}{\nterm{cast}}
+\newcommand{\cofixpointbodies}{\nterm{cofix\_bodies}}
+\newcommand{\cofixpointbody}{\nterm{cofix\_body}}
+\newcommand{\commandtac}{\nterm{tactic\_invocation}}
+\newcommand{\constructor}{\nterm{constructor}}
+\newcommand{\convtactic}{\nterm{conv\_tactic}}
+\newcommand{\declarationkeyword}{\nterm{declaration\_keyword}}
+\newcommand{\declaration}{\nterm{declaration}}
+\newcommand{\definition}{\nterm{definition}}
+\newcommand{\digit}{\nterm{digit}}
+\newcommand{\exteqn}{\nterm{ext\_eqn}}
+\newcommand{\field}{\nterm{field}}
+\newcommand{\firstletter}{\nterm{first\_letter}}
+\newcommand{\fixpg}{\nterm{fix\_pgm}}
+\newcommand{\fixpointbodies}{\nterm{fix\_bodies}}
+\newcommand{\fixpointbody}{\nterm{fix\_body}}
+\newcommand{\fixpoint}{\nterm{fixpoint}}
+\newcommand{\flag}{\nterm{flag}}
+\newcommand{\form}{\nterm{form}}
+\newcommand{\entry}{\nterm{entry}} 
+\newcommand{\proditem}{\nterm{production\_item}} 
+\newcommand{\taclevel}{\nterm{tactic\_level}}
+\newcommand{\tacargtype}{\nterm{tactic\_argument\_type}} 
+\newcommand{\scope}{\nterm{scope}} 
+\newcommand{\delimkey}{\nterm{key}} 
+\newcommand{\optscope}{\nterm{opt\_scope}} 
+\newcommand{\declnotation}{\nterm{decl\_notation}} 
+\newcommand{\symbolentry}{\nterm{symbol}}
+\newcommand{\modifiers}{\nterm{modifiers}}
+\newcommand{\localdef}{\nterm{local\_def}}
+\newcommand{\localdecls}{\nterm{local\_decls}}
+\newcommand{\ident}{\nterm{ident}}
+\newcommand{\accessident}{\nterm{access\_ident}}
+\newcommand{\possiblybracketedident}{\nterm{possibly\_bracketed\_ident}}
+\newcommand{\inductivebody}{\nterm{ind\_body}}
+\newcommand{\inductive}{\nterm{inductive}}
+\newcommand{\naturalnumber}{\nterm{natural}}
+\newcommand{\integer}{\nterm{integer}}
+\newcommand{\multpattern}{\nterm{mult\_pattern}}
+\newcommand{\mutualcoinductive}{\nterm{mutual\_coinductive}}
+\newcommand{\mutualinductive}{\nterm{mutual\_inductive}}
+\newcommand{\nestedpattern}{\nterm{nested\_pattern}}
+\newcommand{\name}{\nterm{name}}
+\newcommand{\num}{\nterm{num}}
+\newcommand{\pattern}{\nterm{pattern}}
+\newcommand{\orpattern}{\nterm{or\_pattern}}
+\newcommand{\intropattern}{\nterm{intro\_pattern}}
+\newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}}
+\newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}}
+\newcommand{\pat}{\nterm{pat}}
+\newcommand{\pgs}{\nterm{pgms}}
+\newcommand{\pg}{\nterm{pgm}}
 %BEGIN LATEX
-\newcommand{\proof}{\textrm{\textsl{proof}}}
+\newcommand{\proof}{\nterm{proof}}
 %END LATEX
-%HEVEA \renewcommand{\proof}{\textrm{\textsl{proof}}}
-\newcommand{\record}{\textrm{\textsl{record}}}
-\newcommand{\rewrule}{\textrm{\textsl{rewriting\_rule}}}
-\newcommand{\sentence}{\textrm{\textsl{sentence}}}
-\newcommand{\simplepattern}{\textrm{\textsl{simple\_pattern}}}
-\newcommand{\sort}{\textrm{\textsl{sort}}}
-\newcommand{\specif}{\textrm{\textsl{specif}}}
-\newcommand{\statement}{\textrm{\textsl{statement}}}
-\newcommand{\str}{\textrm{\textsl{string}}}
-\newcommand{\subsequentletter}{\textrm{\textsl{subsequent\_letter}}}
-\newcommand{\switch}{\textrm{\textsl{switch}}}
-\newcommand{\messagetoken}{\textrm{\textsl{message\_token}}}
-\newcommand{\tac}{\textrm{\textsl{tactic}}}
-\newcommand{\terms}{\textrm{\textsl{terms}}}
-\newcommand{\term}{\textrm{\textsl{term}}}
-\newcommand{\module}{\textrm{\textsl{module}}}
-\newcommand{\modexpr}{\textrm{\textsl{module\_expression}}}
-\newcommand{\modtype}{\textrm{\textsl{module\_type}}}
-\newcommand{\onemodbinding}{\textrm{\textsl{module\_binding}}}
-\newcommand{\modbindings}{\textrm{\textsl{module\_bindings}}}
-\newcommand{\qualid}{\textrm{\textsl{qualid}}}
-\newcommand{\qualidorstring}{\textrm{\textsl{qualid\_or\_string}}}
-\newcommand{\class}{\textrm{\textsl{class}}}
-\newcommand{\dirpath}{\textrm{\textsl{dirpath}}}
-\newcommand{\typedidents}{\textrm{\textsl{typed\_idents}}}
-\newcommand{\type}{\textrm{\textsl{type}}}
-\newcommand{\vref}{\textrm{\textsl{ref}}}
-\newcommand{\zarithformula}{\textrm{\textsl{zarith\_formula}}}
-\newcommand{\zarith}{\textrm{\textsl{zarith}}}
+%HEVEA \renewcommand{\proof}{\nterm{proof}}
+\newcommand{\record}{\nterm{record}}
+\newcommand{\rewrule}{\nterm{rewriting\_rule}}
+\newcommand{\sentence}{\nterm{sentence}}
+\newcommand{\simplepattern}{\nterm{simple\_pattern}}
+\newcommand{\sort}{\nterm{sort}}
+\newcommand{\specif}{\nterm{specif}}
+\newcommand{\statement}{\nterm{statement}}
+\newcommand{\str}{\nterm{string}}
+\newcommand{\subsequentletter}{\nterm{subsequent\_letter}}
+\newcommand{\switch}{\nterm{switch}}
+\newcommand{\messagetoken}{\nterm{message\_token}}
+\newcommand{\tac}{\nterm{tactic}}
+\newcommand{\terms}{\nterm{terms}}
+\newcommand{\term}{\nterm{term}}
+\newcommand{\module}{\nterm{module}}
+\newcommand{\modexpr}{\nterm{module\_expression}}
+\newcommand{\modtype}{\nterm{module\_type}}
+\newcommand{\onemodbinding}{\nterm{module\_binding}}
+\newcommand{\modbindings}{\nterm{module\_bindings}}
+\newcommand{\qualid}{\nterm{qualid}}
+\newcommand{\qualidorstring}{\nterm{qualid\_or\_string}}
+\newcommand{\class}{\nterm{class}}
+\newcommand{\dirpath}{\nterm{dirpath}}
+\newcommand{\typedidents}{\nterm{typed\_idents}}
+\newcommand{\type}{\nterm{type}}
+\newcommand{\vref}{\nterm{ref}}
+\newcommand{\zarithformula}{\nterm{zarith\_formula}}
+\newcommand{\zarith}{\nterm{zarith}}
 \newcommand{\ltac}{\mbox{${\cal L}_{tac}$}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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$}