Suppression SearchNamed finalement redondant avec SearchAbout

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

4 files changed, 0 insertions, 31 deletions

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