SearchAbout: who has never been annoyed by the [ ] syntax ?

 Well, hopefully, that belongs to the past: you should now be able
 to do the very same queries as before, without typing the [ ].
 For instance: SearchAbout plus mult.

 This removal of [ ] is optional, the old syntax is still legal:
  - for compatibility reasons
  - for square bracket lovers
  - for those that have "inside" or "outside" as legal identifier
    in their development and want to search about them.

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

1 files changed, 10 insertions, 12 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 2a0b8051c..ab8e1531f 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -225,8 +225,7 @@ 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).
 
-\item {\tt SearchAbout [ \nelist{\zeroone{-}{\termpatternorstr}}{}
-].}\\
+\item {\tt SearchAbout \nelist{\zeroone{-}{\termpatternorstr}}{}.}\\
 
 \noindent where {\termpatternorstr} is a
 {\termpattern} or a {\str}, or a {\str} followed by a scope
@@ -241,25 +240,24 @@ search excludes the objects that mention that {\termpattern} or that
 {\str}.
 
 \item
-\begin{tabular}[t]{@{}l}
-  {\tt SearchAbout {\termpatternorstr} inside {\module$_1$} \ldots{} {\module$_n$}.} \\
-  {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ]
+  {\tt SearchAbout \nelist{{\termpatternorstr}}{}
     inside {\module$_1$} \ldots{} {\module$_n$}.}
-\end{tabular}
 
 This restricts the search to constructions defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
 \item
-\begin{tabular}[t]{@{}l}
-  {\tt SearchAbout {\termpatternorstr} outside {\module$_1$}...{\module$_n$}.} \\
-  {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ]
+  {\tt SearchAbout \nelist{{\termpatternorstr}}{}
      outside {\module$_1$}...{\module$_n$}.}
-\end{tabular}
 
 This restricts the search to constructions not defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
+\item {\tt SearchAbout [ ... ]. }
+
+For compatibility with older versions, the list of objects to search
+may be enclosed by optional {\tt [  ]} delimiters.
+
 \end{Variants}
 
 \examples
@@ -268,8 +266,8 @@ This restricts the search to constructions not defined in modules
 Require Import ZArith.
 \end{coq_example*}
 \begin{coq_example}
-SearchAbout [ Zmult Zplus "distr" ].
-SearchAbout [ "+"%Z "*"%Z "distr" -positive -Prop].
+SearchAbout Zmult Zplus "distr".
+SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
 SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
 \end{coq_example}