Suppression SearchNamed finalement redondant avec SearchAbout

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

9 files changed, 1 insertions, 40 deletions

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index f4a8580eb2..c86d12ad2a 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -569,9 +569,6 @@ let pcoq_search s l =
   | SearchHead locqid ->
       filtered_search
 	(filter_by_module_from_list l) add_search (Nametab.global locqid)
-  | SearchNamed strings ->
-      raw_search_named
-	(filter_by_module_from_list l) add_search strings
   end;
   search_output_results()
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3d57d24857..3f3c3ba615 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1502,8 +1502,7 @@ let xlate_vernac =
 	| SearchHead id ->
 	    CT_search(loc_qualid_to_ct_ID id, xlate_search_restr x)
 	| SearchRewrite c -> xlate_error "TODO: SearchRewrite"
-	| SearchAbout id -> xlate_error "TODO: SearchAbout"
-	| SearchNamed id -> xlate_error "TODO: SearchNamed")
+	| SearchAbout id -> xlate_error "TODO: SearchAbout")
 
   | (*Record from tactics/Record.v *)
     VernacRecord 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 998a6d2c42..27675758f9 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -108,8 +108,6 @@ GEXTEND Gram
    		 | qid = global -> [SearchRef qid] ];
 	  l = in_or_out_modules -> 
 	  VernacSearch (SearchAbout sl, l)
-      | IDENT "SearchNamed"; sl = LIST1 string; l = in_or_out_modules -> 
-	  VernacSearch (SearchNamed sl, l)
 
       (* TODO: rapprocher Eval et Check *)
       | IDENT "Eval"; r = Tactic.red_expr; "in";
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index c042a24c28..05aea10153 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -526,8 +526,6 @@ GEXTEND Gram
    		 | qid = global -> [SearchRef qid] ];
 	  l = in_or_out_modules -> 
 	  VernacSearch (SearchAbout sl, l)
-      | IDENT "SearchNamed"; sl = LIST1 string; l = in_or_out_modules -> 
-	  VernacSearch (SearchNamed sl, l)
 
       | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = STRING ->
 	  VernacAddMLPath (false, dir)
diff --git a/parsing/search.ml b/parsing/search.ml
index 492028d8bb..5e825ac480 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -222,27 +222,3 @@ let raw_search_about filter_modules display_function l =
 
 let search_about ref inout = 
   raw_search_about (filter_by_module_from_list inout) plain_display ref
-
-(** SearchNamed *)
-
-let close_string s = 
-  if s.[String.length s - 1] = '*' then String.sub s 0 (String.length s - 1)
-  else s^"_"
-
-let occur_string_in_name name s =
-  let l = String.length s + 1 in
-  let l' = String.length name in
-  string_string_contains name (close_string ("_"^s))
-  || l' >= l && String.sub name 0 l = (close_string s)
-  || l' >= l && String.sub name (l'-l) l = ("_"^s)
-
-let raw_search_named filter_modules display_function strings =
-  let filter ref' env typ =
-    filter_modules ref' env typ &&
-    List.for_all (occur_string_in_name (name_of_reference ref')) strings
-  in
-  gen_filtered_search filter display_function
-
-
-let search_named strings inout =
-  raw_search_named (filter_by_module_from_list inout) plain_display strings
diff --git a/parsing/search.mli b/parsing/search.mli
index 851e6431d3..b1f062bba9 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -26,7 +26,6 @@ val search_by_head : global_reference -> dir_path list * bool -> unit
 val search_rewrite : constr_pattern -> dir_path list * bool -> unit
 val search_pattern : constr_pattern -> dir_path list * bool -> unit
 val search_about  : glob_search_about_item list -> dir_path list * bool -> unit
-val search_named  : string list -> dir_path list * bool -> unit
 
 (* The filtering function that is by standard search facilities.
    It can be passed as argument to the raw search functions.
@@ -46,5 +45,3 @@ val raw_search_rewrite : (global_reference -> env -> constr -> bool) ->
 val raw_search_about : (global_reference -> env -> constr -> bool) ->
   (global_reference -> env -> constr -> unit) -> 
       glob_search_about_item list -> unit
-val raw_search_named : (global_reference -> env -> constr -> bool) ->
-  (global_reference -> env -> constr -> unit) -> string list -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d4b6b552e2..5577db4ff9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -903,8 +903,6 @@ let vernac_search s r =
       Search.search_by_head (Nametab.global locqid) r
   | SearchAbout sl ->
       Search.search_about (List.map interp_search_about_item sl) r
-  | SearchNamed strings ->
-      Search.search_named strings r
 
 let vernac_locate = function
   | LocateTerm qid -> msgnl (print_located_qualid qid)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 042845dc6d..e720245b78 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -65,7 +65,6 @@ type searchable =
   | SearchRewrite of pattern_expr
   | SearchHead of reference
   | SearchAbout of search_about_item list
-  | SearchNamed of string list
 
 type locatable =
   | LocateTerm of reference
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index de2f055996..e2a4d22e42 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -158,7 +158,6 @@ let pr_search a b pr_p = match a with
   | 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
-  | SearchNamed sl -> str"SearchNamed" ++ spc() ++ prlist_with_sep spc qsnew sl ++ pr_in_out_modules b
 
 let pr_locality local = if local then str "Local " else str ""