- Added support for subterm matching in SearchAbout.

- Backtrack on precise unfolding of "iff" in "tauto": it has effects on
  the naming of hypotheses (especially when doing "case H" with H of
  type "{x|P<->Q}" since not unfolding will eventually introduce a name
  "i" while unfolding will eventually introduce a name "a" (deep sigh).
- Miscellaneous (error when a plugin is missing, doc hnf, standardization
  of names manipulating type constr_pattern, ...).



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

3 files changed, 49 insertions, 32 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index be5980fe4..89b7350f3 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -47,6 +47,7 @@
 \newcommand{\Rem}{\medskip \noindent {\bf Remark: }}
 \newcommand{\Rems}{\medskip \noindent {\bf Remarks: }}
 \newcommand{\Example}{\medskip \noindent {\bf Example: }}
+\newcommand{\Examples}{\medskip \noindent {\bf Examples: }}
 \newcommand{\Warning}{\medskip \noindent {\bf Warning: }}
 \newcommand{\Warns}{\medskip \noindent {\bf Warnings: }}
 \newcounter{ex}
@@ -60,8 +61,6 @@
 \newenvironment{ErrMsgs}{\ErrMsgx\begin{enumerate}}{\end{enumerate}}
 \newenvironment{Remarks}{\Rems\begin{enumerate}}{\end{enumerate}}
 \newenvironment{Warnings}{\Warns\begin{enumerate}}{\end{enumerate}}
-\newenvironment{Examples}{\medskip\noindent{\bf Examples:}
-\begin{enumerate}}{\end{enumerate}}
 
 %\newcommand{\bd}{\noindent\bf}
 %\newcommand{\sbd}{\vspace{8pt}\noindent\bf}
@@ -191,11 +190,12 @@
 \newcommand{\nestedpattern}{\nterm{nested\_pattern}}
 \newcommand{\name}{\nterm{name}}
 \newcommand{\num}{\nterm{num}}
-\newcommand{\pattern}{\nterm{pattern}}
+\newcommand{\pattern}{\nterm{pattern}} % pattern for pattern-matching
 \newcommand{\orpattern}{\nterm{or\_pattern}}
 \newcommand{\intropattern}{\nterm{intro\_pattern}}
 \newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}}
 \newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}}
+\newcommand{\termpattern}{\nterm{term\_pattern}} % term with holes
 \newcommand{\pat}{\nterm{pat}}
 \newcommand{\pgs}{\nterm{pgms}}
 \newcommand{\pg}{\nterm{pgm}}
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 3f1e517d6..3168f7737 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -134,6 +134,8 @@ environment}\\
     There is no constant in the environment named \qualid.
 \end{ErrMsgs}
 
+\newcommand{\termpatternorstr}{{\termpattern}\textrm{\textsl{-}}{\str}}
+
 \begin{Variants}
 \item {\tt SearchAbout {\str}.}
 
@@ -151,30 +153,32 @@ 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}, or a {\str} followed by a scope delimiting key 
-{\tt \%{\delimkey}}.
+\item {\tt SearchAbout {\termpattern}.}
 
-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}.
+This searches for all statements or types of definition that contains
+a subterm that matches the pattern {\termpattern} (holes of the
+pattern are either denoted by ``{\texttt \_}'' or
+by ``{\texttt ?{\ident}}'' when non linear patterns are expected).
 
-\Example
+\item {\tt SearchAbout [ \nelist{\zeroone{-}{\termpatternorstr}}{}
+].}\\
 
-\begin{coq_example}
-Require Import ZArith.
-SearchAbout [ Zmult Zplus "distr" ].
-\end{coq_example}
+\noindent where {\termpatternorstr} is a
+{\termpattern} or a {\str}, or a {\str} followed by a scope
+delimiting key {\tt \%{\delimkey}}.
+
+This generalization of {\tt SearchAbout} searches for all objects
+whose statement or type contains a subterm matching {\termpattern} (or
+{\qualid} if {\str} is the notation for a reference {\qualid}) and
+whose name contains all {\str} of the request that correspond to valid
+identifiers. If a {\termpattern} or a {\str} is prefixed by ``-'', the
+search excludes the objects that mention that {\termpattern} or that
+{\str}.
 
 \item
 \begin{tabular}[t]{@{}l}
-  {\tt SearchAbout {\term} inside {\module$_1$} \ldots{} {\module$_n$}.} \\
-  {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
+  {\tt SearchAbout {\termpatternorstr} inside {\module$_1$} \ldots{} {\module$_n$}.} \\
+  {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ]
     inside {\module$_1$} \ldots{} {\module$_n$}.}
 \end{tabular}
 
@@ -183,8 +187,8 @@ This restricts the search to constructions defined in modules
 
 \item
 \begin{tabular}[t]{@{}l}
-  {\tt SearchAbout {\term} outside {\module$_1$}...{\module$_n$}.} \\
-  {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
+  {\tt SearchAbout {\termpatternorstr} outside {\module$_1$}...{\module$_n$}.} \\
+  {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ]
      outside {\module$_1$}...{\module$_n$}.}
 \end{tabular}
 
@@ -193,11 +197,25 @@ This restricts the search to constructions not defined in modules
 
 \end{Variants}
 
-\subsection[\tt SearchPattern {\term}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}}
+\Examples
+
+\begin{coq_example*}
+Require Import ZArith.
+\end{coq_example*}
+\begin{coq_example}
+SearchAbout [ Zmult Zplus "distr" ].
+SearchAbout [ "+"%Z "*"%Z "distr" -positive -Prop].
+SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
+\end{coq_example}
+
+\subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}}
 
 This command displays the name and type of all theorems of the current
 context whose statement's conclusion matches the expression {\term}
-where holes in the latter are denoted by ``{\texttt \_}''.
+where holes in the latter are denoted by ``{\texttt \_}''. It is a
+variant of {\tt SearchAbout {\termpattern}} that does not look for
+subterms but searches for statements whose conclusion has exactly the
+expected form.
 
 \begin{coq_example}
 Require Import Arith.
@@ -215,13 +233,12 @@ SearchPattern (?X1 + _ = _ + ?X1).
 
 \begin{Variants}
 \item {\tt SearchPattern {\term} inside
-{\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} inside
-\ldots{}}
+{\module$_1$} \ldots{} {\module$_n$}.}
 
 This restricts the search to constructions defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
-\item {\tt SearchPattern {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} outside \ldots{}}
+\item {\tt SearchPattern {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}
 
 This restricts the search to constructions not defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
@@ -232,7 +249,7 @@ This restricts the search to constructions not defined in modules
 
 This command displays the name and type of all theorems of the current
 context whose statement's conclusion is an equality of which one side matches
-the expression {\term =}. Holes in {\term} are denoted by ``{\texttt \_}''.
+the expression {\term}. Holes in {\term} are denoted by ``{\texttt \_}''.
 
 \begin{coq_example}
 Require Import Arith.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 07d9df9c5..f5568455f 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1269,9 +1269,9 @@ $\beta\iota\zeta$-reduction rules.
 \tacindex{hnf}}
 
 This tactic applies to any goal. It replaces the current goal with its
-head normal form according to the $\beta\delta\iota\zeta$-reduction rules.
-{\tt hnf} does not produce a real head normal form but either a
-product or an applicative term in head normal form or a variable.
+head normal form according to the $\beta\delta\iota\zeta$-reduction
+rules, i.e.  it reduces the head of the goal until it becomes a
+product or an irreducible term.
 
 \Example
 The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}.