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
---
 printing/ppvernac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 415d703162..427317a45a 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 ()
-- 
cgit v1.2.3