From 9b24b6d763bb2c7975cd2b93364d7647fd660598 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Apr 2013 18:33:16 +0000
Subject: 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
---
 parsing/g_vernac.ml4 | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 56abf3e1c4..004dbab7b4 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)
 
-- 
cgit v1.2.3