Renaming SearchAbout into Search and Search into SearchHead.

I hope I did not forget any place to change.

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

14 files changed, 114 insertions, 98 deletions

diff --git a/CHANGES b/CHANGES
index 416f0a117..6b6892e1d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,9 @@ Vernacular commands
 - The "Open Scope" command can now be given also a delimiter (e.g. Z).
 - The "Definition" command now allows the "Local" modifier.
 - The "Let" command can now define local (co)fixpoints.
+- Command "Search" has been renamed into "SearchHead". The command
+  name "Search" now behaves like former "SearchAbout". The latter name
+  is deprecated.
 
 Specification Language
 
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index e0c6c868f..ec640f4ef 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -147,16 +147,16 @@ arguments.
 
 
 We call \emph{query} any vernacular command that do not change the
-current state, such as \verb|Check|, \verb|SearchAbout|, etc. Those
+current state, such as \verb|Check|, \verb|Search|, etc. Those
 commands are of course useless during compilation of a file, hence
 should not be included in scripts. To run such commands without
 writing them in the script, \CoqIDE{} offers another input window
 called the \emph{query window}. This window can be displayed on
 demand, either by using the \texttt{Window} menu, or directly using
 shortcuts given in the \texttt{Queries} menu. Indeed, with \CoqIDE{}
-the simplest way to perform a \texttt{SearchAbout} on some identifier
+the simplest way to perform a \texttt{Search} on some identifier
 is to select it using the mouse, and pressing \verb|F2|. This will
-both make appear the query window and run the \texttt{SearchAbout} in
+both make appear the query window and run the \texttt{Search} in
 it, displaying the result. Shortcuts \verb|F3| and \verb|F4| are for
 \verb|Check| and \verb|Print| respectively.
 Figure~\ref{fig:querywindow} displays the query window after selection
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 0126e686b..a543561b5 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -164,37 +164,7 @@ relies.
   Displays all assumptions and constants {\qualid} relies on.
 \end{Variants}
 
-\subsection[\tt Search {\term}.]{\tt Search {\term}.\comindex{Search}}
-This command displays the name and type of all theorems of the current
-context whose statement's conclusion has the form {\tt ({\term} t1 ..
-  tn)}.  This command is useful to remind the user of the name of
-library lemmas.
-
-\begin{coq_example}
-Search le.
-Search (@eq bool).
-\end{coq_example}
-
-\begin{Variants}
-\item
-{\tt Search} {\term} {\tt inside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
-
-This restricts the search to constructions defined in modules
-{\module$_1$} \ldots{} {\module$_n$}.
-
-\item {\tt Search} {\term} {\tt outside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
-
-This restricts the search to constructions not defined in modules
-{\module$_1$} \ldots{} {\module$_n$}.
-
-\begin{ErrMsgs}
-\item \errindex{Module/section \module{} not found}
-No module \module{} has been required (see Section~\ref{Require}).
-\end{ErrMsgs}
-
-\end{Variants}
-
-\subsection[\tt SearchAbout {\qualid}.]{\tt SearchAbout {\qualid}.\comindex{SearchAbout}}
+\subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}}
 This command displays the name and type of all objects (theorems,
 axioms, etc) of the current context whose statement contains \qualid.
 This command is useful to remind the user of the name of library
@@ -209,36 +179,36 @@ environment}\\
 \newcommand{\termpatternorstr}{{\termpattern}\textrm{\textsl{-}}{\str}}
 
 \begin{Variants}
-\item {\tt SearchAbout {\str}.}
+\item {\tt Search {\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
+Section~\ref{Notation}), the command works like {\tt Search
 {\qualid}}.
 
-\item {\tt SearchAbout {\str}\%{\delimkey}.}
+\item {\tt Search {\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 {\termpattern}.}
+\item {\tt Search {\termpattern}.}
 
 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).
 
-\item {\tt SearchAbout \nelist{\zeroone{-}{\termpatternorstr}}{}.}\\
+\item {\tt Search \nelist{\zeroone{-}{\termpatternorstr}}{}.}\\
 
 \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
+This generalization of {\tt Search} 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
@@ -247,24 +217,19 @@ search excludes the objects that mention that {\termpattern} or that
 {\str}.
 
 \item
-  {\tt SearchAbout} \nelist{{\termpatternorstr}}{}
+  {\tt Search} \nelist{{\termpatternorstr}}{}
     {\tt inside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
 
 This restricts the search to constructions defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
 \item
-  {\tt SearchAbout \nelist{{\termpatternorstr}}{}
+  {\tt Search \nelist{{\termpatternorstr}}{}
      outside {\module$_1$}...{\module$_n$}.}
 
 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
@@ -273,17 +238,61 @@ may be enclosed by optional {\tt [  ]} delimiters.
 Require Import ZArith.
 \end{coq_example*}
 \begin{coq_example}
-SearchAbout Z.mul Z.add "distr".
-SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
-SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
+Search Z.mul Z.add "distr".
+Search "+"%Z "*"%Z "distr" -positive -Prop.
+Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 \end{coq_example}
 
+\Warning \comindex{SearchAbout} Up to Coq version 8.4, {\tt Search}
+had the behavior of current {\tt SearchHead} and the behavior of
+current {\tt Search} was obtained with command {\tt SearchAbout}. For
+compatibility, the deprecated name {\tt SearchAbout} can still be used
+as a synonym of {\tt Search}. For compatibility, the list of objects to
+search when using {\tt SearchAbout} may also be enclosed by optional
+{\tt [ ]} delimiters.
+
+\subsection[\tt SearchHead {\term}.]{\tt SearchHead {\term}.\comindex{SearchHead}}
+This command displays the name and type of all theorems of the current
+context whose statement's conclusion has the form {\tt ({\term} t1 ..
+  tn)}.  This command is useful to remind the user of the name of
+library lemmas.
+
+\begin{coq_example*}
+Reset Initial.
+\end{coq_example*}
+
+\begin{coq_example}
+SearchHead le.
+SearchHead (@eq bool).
+\end{coq_example}
+
+\begin{Variants}
+\item
+{\tt SearchHead} {\term} {\tt inside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
+
+This restricts the search to constructions defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\item {\tt SearchHead} {\term} {\tt outside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
+
+This restricts the search to constructions not defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\begin{ErrMsgs}
+\item \errindex{Module/section \module{} not found}
+No module \module{} has been required (see Section~\ref{Require}).
+\end{ErrMsgs}
+
+\end{Variants}
+
+\Warning Up to Coq version 8.4, {\tt SearchHead} was named {\tt Search}.
+
 \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 or last hypothesis and conclusion
 matches the expression {\term} where holes in the latter are denoted
-by ``{\texttt \_}''. It is a variant of {\tt SearchAbout
+by ``{\texttt \_}''. It is a variant of {\tt Search
   {\termpattern}} that does not look for subterms but searches for
 statements whose conclusion has exactly the expected form, or whose
 statement finishes by the given series of hypothesis/conclusion.
@@ -344,7 +353,7 @@ This restricts the search to constructions not defined in modules
 \end{Variants}
 
 \subsubsection{Nota Bene:}
-For the {\tt Search}, {\tt SearchAbout}, {\tt SearchPattern} and
+For the {\tt Search}, {\tt SearchHead}, {\tt SearchPattern} and
 {\tt SearchRewrite} queries, it is possible to globally filter
 the search results via the command
 {\tt Add Search Blacklist "substring1"}.
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 43c8bf620..5907edb61 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -1539,17 +1539,17 @@ you should use \verb:Require Export M: in your module \verb:N:.
 
 It is often difficult to remember the names of all lemmas and
 definitions available in the current context, especially if large
-libraries have been loaded. A convenient \verb:SearchAbout: command
+libraries have been loaded. A convenient \verb:Search: command
 is available to lookup all known facts 
 concerning a given predicate. For instance, if you want to know all the
 known lemmas about the less or equal relation, just ask:
 \begin{coq_example}
-SearchAbout le.
+Search le.
 \end{coq_example}
-Another command \verb:Search: displays only lemmas where the searched
+Another command \verb:SearchHead: displays only lemmas where the searched
 predicate appears at the head position in the conclusion.
 \begin{coq_example}
-Search le.
+SearchHead le.
 \end{coq_example}
 
 A new and more convenient search tool is \textsf{SearchPattern}
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 26dbcb125..ae39a1249 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -207,7 +207,8 @@ let state_preserving = [
   "Recursive Extraction Library";
 
   "Search";
-  "SearchAbout";
+  "SearchAbout (* deprecated *)";
+  "SearchHead";
   "SearchPattern";
   "SearchRewrite";
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 8429a9b07..616358789 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -626,7 +626,7 @@ let otherquery command _ =
     Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore
 
 let query command _ =
-  if command = "SearchAbout"
+  if command = "Search" || command = "SearchAbout"
   then searchabout ()
   else otherquery command ()
 
@@ -1054,7 +1054,7 @@ let build_ui () =
   let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in
   menu queries_menu [
     item "Queries" ~label:"_Queries";
-    qitem "SearchAbout" (Some "F2");
+    qitem "Search" (Some "F2");
     qitem "Check" (Some "F3");
     qitem "Print" (Some "F4");
     qitem "About" (Some "F5");
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index d88f623ef..8732cd83b 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -110,7 +110,7 @@ let init () =
     %s
   </menu>
   <menu action='Queries'>
-    <menuitem action='SearchAbout' />
+    <menuitem action='Search' />
     <menuitem action='Check' />
     <menuitem action='Print' />
     <menuitem action='About' />
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index e21cc0aa0..319342e91 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -253,10 +253,10 @@ class finder (view : GText.view) =
 class info (coqtop : Coq.coqtop) (view : GText.view) (msg_view : Wg_MessageView.message_view) =
 
   let widget = GPack.vbox () in
-  (* SearchAbout part *)
+  (* Search part *)
   let query_box = GPack.hbox ~packing:widget#add () in
   let _ =
-    GMisc.label ~text:"SearchAbout:"
+    GMisc.label ~text:"Search:"
       ~xalign:1.0
       ~packing:query_box#pack ()
   in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 56abf3e1c..004dbab7b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -766,15 +766,18 @@ GEXTEND Gram
       | IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid)
 
       (* Searching the environment *)
-      | IDENT "Search"; c = constr_pattern; l = in_or_out_modules ->
+      | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchHead c, l)
       | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchPattern c, l)
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchRewrite c, l)
+      | IDENT "Search"; s = searchabout_query; l = searchabout_queries ->
+	  let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m)
+      (* compatibility: SearchAbout *)
       | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries ->
 	  let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m)
-      (* compatibility format of SearchAbout, with "[ ... ]" *)
+      (* compatibility: SearchAbout with "[ ... ]" *)
       | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]";
 	  l = in_or_out_modules -> VernacSearch (SearchAbout sl, l)
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 415d70316..427317a45 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -126,10 +126,10 @@ let pr_search_about (b,c) =
   | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
 let pr_search a b pr_p = match a with
-  | SearchHead c -> str"Search" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+  | SearchHead c -> str"SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
-  | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b
+  | SearchAbout sl -> str"Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
 
 let pr_locality_full = function
   | None -> mt ()
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 2a22a89b6..120c6a4ea 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,29 +1,29 @@
-le_S: forall n m : nat, n <= m -> n <= S m
 le_n: forall n : nat, n <= n
+le_S: forall n m : nat, n <= m -> n <= S m
 le_pred: forall n m : nat, n <= m -> pred n <= pred m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
-false: bool
 true: bool
-xorb: bool -> bool -> bool
+false: bool
+andb: bool -> bool -> bool
 orb: bool -> bool -> bool
-negb: bool -> bool
 implb: bool -> bool -> bool
-andb: bool -> bool -> bool
-pred_Sn: forall n : nat, n = pred (S n)
-plus_n_Sm: forall n m : nat, S (n + m) = n + S m
-plus_n_O: forall n : nat, n = n + 0
-plus_Sn_m: forall n m : nat, S n + m = S (n + m)
-plus_O_n: forall n : nat, 0 + n = n
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-mult_n_O: forall n : nat, 0 = n * 0
-min_r: forall n m : nat, m <= n -> min n m = m
-min_l: forall n m : nat, n <= m -> min n m = n
-max_r: forall n m : nat, n <= m -> max n m = m
-max_l: forall n m : nat, m <= n -> max n m = n
+xorb: bool -> bool -> bool
+negb: bool -> bool
+eq_S: forall x y : nat, x = y -> S x = S y
 f_equal_pred: forall x y : nat, x = y -> pred x = pred y
+pred_Sn: forall n : nat, n = pred (S n)
+eq_add_S: forall n m : nat, S n = S m -> n = m
 f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+plus_n_O: forall n : nat, n = n + 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
 f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-eq_add_S: forall n m : nat, S n = S m -> n = m
-eq_S: forall x y : nat, x = y -> S x = S y
+mult_n_O: forall n : nat, 0 = n * 0
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+max_l: forall n m : nat, m <= n -> max n m = n
+max_r: forall n m : nat, n <= m -> max n m = m
+min_l: forall n m : nat, n <= m -> min n m = n
+min_r: forall n m : nat, m <= n -> min n m = m
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index f1489f22a..4ef263473 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -1,5 +1,5 @@
 (* Some tests of the Search command *)
 
-Search le.				(* app nodes *)
-Search bool. 				(* no apps *)
-Search (@eq nat).			(* complex pattern *)
+SearchHead le.				(* app nodes *)
+SearchHead bool. 				(* no apps *)
+SearchHead (@eq nat).			(* complex pattern *)
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index d546f84da..6595302e1 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,32 +1,32 @@
-false: bool
 true: bool
-xorb: bool -> bool -> bool
+false: bool
+andb: bool -> bool -> bool
 orb: bool -> bool -> bool
-negb: bool -> bool
 implb: bool -> bool -> bool
-andb: bool -> bool -> bool
-S: nat -> nat
+xorb: bool -> bool -> bool
+negb: bool -> bool
 O: nat
+S: nat -> nat
+length: forall A : Type, list A -> nat
 pred: nat -> nat
 plus: nat -> nat -> nat
 mult: nat -> nat -> nat
 minus: nat -> nat -> nat
-min: nat -> nat -> nat
 max: nat -> nat -> nat
-length: forall A : Type, list A -> nat
+min: nat -> nat -> nat
 
 S: nat -> nat
 pred: nat -> nat
 plus: nat -> nat -> nat
 mult: nat -> nat -> nat
 minus: nat -> nat -> nat
-min: nat -> nat -> nat
 max: nat -> nat -> nat
+min: nat -> nat -> nat
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
-le_n: forall n : nat, n <= n
 identity_refl: forall (A : Type) (a : A), identity a a
-eq_refl: forall (A : Type) (x : A), x = x
 iff_refl: forall A : Prop, A <-> A
+eq_refl: forall (A : Type) (x : A), x = x
+le_n: forall n : nat, n <= n
 pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 61c18f9e4..6582b8c70 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -41,7 +41,7 @@ let is_keyword =
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
-      "Search"; "SearchAbout"; "SearchRewrite";
+      "Search"; "SearchAbout"; "SearchHead"; "SearchPattern"; "SearchRewrite";
       "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope"; "Inline";