Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?

mechanism with the SearchAbout one. Searches may be slower, but this
is unlikely to be noticed. In addition, according to Hugo, the
Libtype summary was imposing a noticeable time penalty without
any real advantage.

Now Search and SearchPattern are the same. The documentation was not
really clear about the difference between both, except that Search
was restricted to closed terms. This is an artificial restriction by
now.

Fixing #2815 btw.

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

8 files changed, 155 insertions, 328 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a677eb93ed..1d25bc1d9c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1685,15 +1685,15 @@ let interp_open_constr sigma env c =
 let interp_open_constr_patvar sigma env c =
   let raw = intern_gen (OfType None) sigma env c ~allow_patvar:true in
   let sigma = ref sigma in
-  let evars = ref (Gmap.empty : (Id.t,glob_constr) Gmap.t) in
+  let evars = ref (Id.Map.empty : glob_constr Id.Map.t) in
   let rec patvar_to_evar r = match r with
     | GPatVar (loc,(_,id)) ->
-	( try Gmap.find id !evars
+	( try Id.Map.find id !evars
 	  with Not_found ->
 	    let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in
 	    let ev = Evarutil.e_new_evar sigma env ev in
 	    let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
-	    evars := Gmap.add id rev !evars;
+	    evars := Id.Map.add id rev !evars;
 	    rev
 	)
     | _ -> map_glob_constr patvar_to_evar r in
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 955b42700c..b2a9aebdc4 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -32,6 +32,8 @@ type instance_decl_function = global_reference -> rel_context -> constr list ->
  * Search algorithm
  *)
 
+let reduce x = x
+
 let rec subst_evar evar def n c =
   match kind_of_term c with
     | Evar (e,_) when Int.equal e evar -> lift n def
@@ -65,8 +67,8 @@ let rec safe_define evm ev c =
     | Evd.Evar_defined def ->
 	define_subst evm (Termops.filtering [] Reduction.CUMUL def c)
     | Evd.Evar_empty ->
-	let t = Libtypes.reduce (Typing.type_of (Global.env()) evm c) in
-	let u = Libtypes.reduce (evar_concl evi) in
+	let t = reduce (Typing.type_of (Global.env()) evm c) in
+	let u = reduce (evar_concl evi) in
 	let evm = subst_evar_in_evm ev c evm in
 	define_subst (Evd.define ev c evm) (Termops.filtering [] Reduction.CUMUL t u)
 
@@ -94,10 +96,14 @@ module SubstSet : Set.S with type elt = Termops.subst
 		     let compare = Int.Map.compare (Pervasives.compare)
 	      end)
 
+let search_concl typ = assert false
+(** FIXME: if one ever wants to maintain this code, he has to plug the Search
+    machinery into this assertion failure. *)
+
 (* searches instatiations in the library for just one evar [ev] of a
    signature. [k] is called on each resulting signature *)
 let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) =
-  let ev_typ = Libtypes.reduce (evar_concl evi) in
+  let ev_typ = reduce (evar_concl evi) in
   let sort_is_prop = is_Prop (Typing.type_of (Global.env()) evm (evar_concl evi)) in
 (*  msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Pp.int ev);*)
   let substs = ref SubstSet.empty in
@@ -116,7 +122,7 @@ let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) =
 	  if sort_is_prop && SubstSet.mem s !substs then raise Exit;
 	  substs := SubstSet.add s !substs
 	with Termops.CannotFilter -> ()
-    ) (Libtypes.search_concl ev_typ)
+    ) (search_concl ev_typ)
   with Exit -> ()
 
 let evm_fold_rev f evm acc =
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
deleted file mode 100644
index 0866db092e..0000000000
--- a/toplevel/libtypes.ml
+++ /dev/null
@@ -1,110 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Term
-open Summary
-open Libobject
-open Globnames
-(*
- * Module construction
- *)
-
-(* let reduce c = Reductionops.head_unfold_under_prod *)
-(*   (Auto.Hint_db.transparent_state (Auto.searchtable_map "typeclass_instances")) *)
-(*   (Global.env()) Evd.empty c *)
-
-let reduce c = c
-
-module TypeDnet = Term_dnet.Make
-  (struct
-     type t = Globnames.global_reference
-     let compare = RefOrdered.compare
-     let subst s gr = fst (Globnames.subst_global s gr)
-     let constr_of = Global.type_of_global
-   end)
-  (struct let reduce = reduce
-	  let direction = false
-   end)
-
-type result = Globnames.global_reference * (constr*existential_key) * Termops.subst
-
-let all_types = ref TypeDnet.empty
-let defined_types = ref TypeDnet.empty
-
-(*
- * Bookeeping & States
- *)
-
-let freeze () =
-  (!all_types,!defined_types)
-
-let unfreeze (lt,dt) =
-  all_types := lt;
-  defined_types := dt
-
-let init () =
-  all_types := TypeDnet.empty;
-  defined_types := TypeDnet.empty
-
-let _ =
-  declare_summary "type-library-state"
-    { freeze_function = freeze;
-      unfreeze_function = unfreeze;
-      init_function = init }
-
-let load (_,d) =
-(*  Profile.print_logical_stats !all_types;
-  Profile.print_logical_stats d;*)
-  all_types := TypeDnet.union d !all_types
-
-let subst s t = TypeDnet.subst s t
-(*
-let subst_key = Profile.declare_profile "subst"
-let subst a b = Profile.profile2 subst_key TypeDnet.subst a b
-
-let load_key = Profile.declare_profile "load"
-let load a = Profile.profile1 load_key load a
-*)
-let input : TypeDnet.t -> obj =
-  declare_object
-    { (default_object "LIBTYPES") with
-	load_function = (fun _ -> load);
-	subst_function = (fun (s,t) -> subst s t);
-	classify_function = (fun x -> Substitute x)
-    }
-
-let update () = Lib.add_anonymous_leaf (input !defined_types)
-
-(*
- * Search interface
- *)
-
-let search_pattern pat = TypeDnet.search_pattern !all_types pat
-let search_concl pat = TypeDnet.search_concl !all_types pat
-let search_head_concl pat = TypeDnet.search_head_concl !all_types pat
-let search_eq_concl eq pat = TypeDnet.search_eq_concl !all_types eq pat
-
-let add typ gr =
-  defined_types := TypeDnet.add typ gr !defined_types;
-  all_types := TypeDnet.add typ gr !all_types
-(*
-let add_key = Profile.declare_profile "add"
-let add a b = Profile.profile1 add_key add a b
-*)
-
-(*
- * Hooks declaration
- *)
-
-let _ = Declare.add_cache_hook
-  ( fun sp ->
-      let gr = Nametab.global_of_path sp in
-      let ty = Global.type_of_global gr in
-      add ty gr )
-
-let _ = Declaremods.set_end_library_hook update
diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli
deleted file mode 100644
index a4ce70e979..0000000000
--- a/toplevel/libtypes.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Term
-
-(** Persistent library of all declared object, indexed by their types 
-    (uses Dnets) *)
-
-(** results are the reference of the object, together with a context
-(constr+evar) and a substitution under this context *)
-type result = Globnames.global_reference * (constr*existential_key) * Termops.subst
-
-(** this is the reduction function used in the indexing process *)
-val reduce : types -> types
-
-(** The different types of search available. 
-    See term_dnet.mli for more explanations *)
-val search_pattern : types -> result list
-val search_concl : types -> result list
-val search_head_concl : types -> result list
-val search_eq_concl : constr -> types -> result list
diff --git a/toplevel/search.ml b/toplevel/search.ml
index c492f077d1..23cff9931e 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -15,7 +15,6 @@ open Declarations
 open Libobject
 open Environ
 open Pattern
-open Matching
 open Printer
 open Libnames
 open Globnames
@@ -34,16 +33,17 @@ module SearchBlacklist =
       let synchronous = true
      end)
 
-(* The functions print_constructors and crible implement the behavior needed
-   for the Coq searching commands.
+(* The functions iter_constructors and iter_declarations implement the behavior
+   needed for the Coq searching commands.
    These functions take as first argument the procedure
    that will be called to treat each entry.  This procedure receives the name
    of the object, the assumptions that will make it possible to print its type,
    and the constr term that represent its type. *)
 
-let print_constructors indsp fn env nconstr =
+let iter_constructors indsp fn env nconstr =
   for i = 1 to nconstr do
-    fn (ConstructRef (indsp,i)) env (Inductiveops.type_of_constructor env (indsp,i))
+    let typ = Inductiveops.type_of_constructor env (indsp, i) in
+    fn (ConstructRef (indsp, i)) env typ
   done
 
 let rec head_const c = match kind_of_term c with
@@ -53,52 +53,36 @@ let rec head_const c = match kind_of_term c with
   | Cast (d,_,_)   -> head_const d
   | _            -> c
 
-(* General search, restricted to head constant if [only_head] *)
-
-let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
+(* General search over declarations *)
+let iter_declarations (fn : global_reference -> env -> constr -> unit) =
   let env = Global.env () in
-  let crible_rec (sp,kn) lobj = match object_tag lobj with
-    | "VARIABLE" ->
-	(try
-	   let (id,_,typ) = Global.lookup_named (basename sp) in
-           begin match refopt with
-           | None ->
-             fn (VarRef id) env typ
-           | Some r when eq_constr (head_const typ) (constr_of_global r) ->
-	     fn (VarRef id) env typ
-           | _ -> ()
-           end
-	 with Not_found -> (* we are in a section *) ())
-    | "CONSTANT" ->
-	let cst = Global.constant_of_delta_kn kn in
-	let typ = Typeops.type_of_constant env cst in
-        begin match refopt with
-        | None ->
-          fn (ConstRef cst) env typ
-        | Some r when eq_constr (head_const typ) (constr_of_global r) ->
-          fn (ConstRef cst) env typ
-        | _ -> ()
-        end
-    | "INDUCTIVE" ->
-	let mind = Global.mind_of_delta_kn kn in
-        let mib = Global.lookup_mind mind in
-        (match refopt with
-	  | Some (IndRef ((kn',tyi) as ind)) when eq_mind mind kn' ->
-	      print_constructors ind fn env
-	        (Array.length (mib.mind_packets.(tyi).mind_user_lc))
-          | Some _ -> ()
-	  | _ ->
-              Array.iteri
-	        (fun i mip -> print_constructors (mind,i) fn env
-	          (Array.length mip.mind_user_lc)) mib.mind_packets)
-    | _ -> ()
+  let iter_obj (sp, kn) lobj = match object_tag lobj with
+  | "VARIABLE" ->
+    begin try
+      let (id, _, typ) = Global.lookup_named (basename sp) in
+      fn (VarRef id) env typ
+    with Not_found -> (* we are in a section *) () end
+  | "CONSTANT" ->
+    let cst = Global.constant_of_delta_kn kn in
+    let typ = Typeops.type_of_constant env cst in
+    fn (ConstRef cst) env typ
+  | "INDUCTIVE" ->
+    let mind = Global.mind_of_delta_kn kn in
+    let mib = Global.lookup_mind mind in
+    let iter_packet i mip =
+      let ind = (mind, i) in
+      let typ = Inductiveops.type_of_inductive env ind in
+      let () = fn (IndRef ind) env typ in
+      let len = Array.length mip.mind_user_lc in
+      iter_constructors ind fn env len
+    in
+    Array.iteri iter_packet mib.mind_packets
+  | _ -> ()
   in
-  try
-    Declaremods.iter_all_segments crible_rec
-  with Not_found ->
-    ()
+  try Declaremods.iter_all_segments iter_obj
+  with Not_found -> ()
 
-let crible ref = gen_crible (Some ref)
+let generic_search = iter_declarations
 
 (* Fine Search. By Yves Bertot. *)
 
@@ -109,7 +93,9 @@ let rec head c =
   | LetIn (_,_,_,c) -> head c
   | _              -> c
 
-let xor a b = (a or b) & (not (a & b))
+let xor a b = (a || b) && (not (a && b))
+
+(** Standard display *)
 
 let plain_display accu ref a c =
   let pc = pr_lconstr_env a c in
@@ -118,143 +104,114 @@ let plain_display accu ref a c =
 
 let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l)
 
-let filter_by_module (module_list:DirPath.t list) (accept:bool)
-  (ref:global_reference) _ _ =
-    let sp = path_of_global ref in
-    let sl = dirpath sp in
-    let rec filter_aux = function
-      | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl)
-      | [] -> true
-    in
-    xor accept (filter_aux module_list)
-
-let gref_eq = Coqlib.glob_eq
-let c_eq = mkInd (Globnames.destIndRef gref_eq)
-
-let mk_rewrite_pattern1 eq pattern =
-  PApp (PRef eq, [| PMeta None; pattern; PMeta None |])
-
-let mk_rewrite_pattern2 eq pattern =
-  PApp (PRef eq, [| PMeta None; PMeta None; pattern |])
-
-let pattern_filter pat _ a c =
-  try
-    try
-      is_matching pat (head c)
-    with e when Errors.noncritical e ->
-      is_matching
-	pat (head (Typing.type_of (Global.env()) Evd.empty c))
-    with UserError _ ->
-      false
-
-let filtered_search filter_function display_function ref =
-  crible ref
-    (fun s a c -> if filter_function s a c then display_function s a c)
-
-let rec id_from_pattern = function
-  | PRef gr -> gr
-(* should be appear as a PRef (VarRef sp) !!
-  | PVar id -> Nametab.locate (make_qualid [] (Id.to_string id))
- *)
-  | PApp (p,_) -> id_from_pattern p
-  | _ -> error "The pattern is not simple enough."
-
-let raw_pattern_search extra_filter display_function pat =
-  let name = id_from_pattern pat in
-  filtered_search
-    (fun s a c -> (pattern_filter pat s a c) & extra_filter s a c)
-    display_function name
-
-let raw_search_rewrite extra_filter display_function pattern =
-  filtered_search
-    (fun s a c ->
-       ((pattern_filter (mk_rewrite_pattern1 gref_eq pattern) s a c) ||
-        (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c))
-       && extra_filter s a c)
-    display_function gref_eq
-
-let raw_search_by_head extra_filter display_function pattern =
-  Errors.todo "raw_search_by_head"
+(** Filters *)
 
-let name_of_reference ref = Id.to_string (basename_of_global ref)
+(** This function tries to see whether the conclusion matches a pattern. *)
+(** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
+let rec pattern_filter pat ref env typ =
+  let typ = strip_outer_cast typ in
+  if Matching.is_matching pat typ then true
+  else match kind_of_term typ with
+  | Prod (_, _, typ)
+  | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ
+  | _ -> false
 
 let full_name_of_reference ref =
   let (dir,id) = repr_path (path_of_global ref) in
   DirPath.to_string dir ^ "." ^ Id.to_string id
 
-(*
- * functions to use the new Libtypes facility
- *)
+(** Whether a reference is blacklisted *)
+let blacklist_filter ref env typ =
+  let name = full_name_of_reference ref in
+  let l = SearchBlacklist.elements () in
+  let is_not_bl str = not (String.string_contains ~where:name ~what:str) in
+  List.for_all is_not_bl l
 
-let raw_search search_function extra_filter display_function pat =
-  let env = Global.env() in
-  List.iter
-    (fun (gr,_,_) ->
-       let typ = Global.type_of_global gr in
-       if extra_filter gr env typ then
-	 display_function gr env typ
-    ) (search_function pat)
+let module_filter (mods, outside) ref env typ =
+  let sp = path_of_global ref in
+  let sl = dirpath sp in
+  let is_outside md = not (is_dirpath_prefix_of md sl) in
+  let is_inside md = is_dirpath_prefix_of md sl in
+  if outside then List.for_all is_outside mods
+  else List.is_empty mods || List.exists is_inside mods
 
-let text_pattern_search extra_filter pat =
-  let ans = ref [] in
-  raw_search Libtypes.search_concl extra_filter (plain_display ans) pat;
-  format_display !ans
+(** SearchPattern *)
 
-let text_search_rewrite extra_filter pat =
+let search_pattern pat mods =
   let ans = ref [] in
-  raw_search (Libtypes.search_eq_concl c_eq) extra_filter (plain_display ans) pat;
+  let filter ref env typ =
+    let f_module = module_filter mods ref env typ in
+    let f_blacklist = blacklist_filter ref env typ in
+    let f_pattern () = pattern_filter pat ref env typ in
+    f_module && f_pattern () && f_blacklist
+  in
+  let iter ref env typ =
+    if filter ref env typ then plain_display ans ref env typ
+  in
+  let () = generic_search iter in
   format_display !ans
 
-let text_search_by_head extra_filter pat =
-  let ans = ref [] in
-  raw_search Libtypes.search_head_concl extra_filter (plain_display ans) pat;
-  format_display !ans
+(** SearchRewrite *)
 
-let filter_by_module_from_list = function
-  | [], _ -> (fun _ _ _ -> true)
-  | l, outside -> filter_by_module l (not outside)
+let eq = Coqlib.glob_eq
 
-let filter_blacklist gr _ _ =
-  let name = full_name_of_reference gr in
-  let l = SearchBlacklist.elements () in
-  List.for_all (fun str -> not (String.string_contains ~where:name ~what:str)) l
+let rewrite_pat1 pat =
+  PApp (PRef eq, [| PMeta None; pat; PMeta None |])
 
-let (&&&&&) f g x y z = f x y z && g x y z
+let rewrite_pat2 pat =
+  PApp (PRef eq, [| PMeta None; PMeta None; pat |])
 
-let search_by_head pat inout =
-  text_search_by_head (filter_by_module_from_list inout &&&&& filter_blacklist) pat
-
-let search_rewrite pat inout =
-  text_search_rewrite (filter_by_module_from_list inout &&&&& filter_blacklist) pat
+let search_rewrite pat mods =
+  let pat1 = rewrite_pat1 pat in
+  let pat2 = rewrite_pat2 pat in
+  let ans = ref [] in
+  let filter ref env typ =
+    let f_module = module_filter mods ref env typ in
+    let f_blacklist = blacklist_filter ref env typ in
+    let f_pattern () =
+      pattern_filter pat1 ref env typ ||
+      pattern_filter pat2 ref env typ
+    in
+    f_module && f_pattern () && f_blacklist
+  in
+  let iter ref env typ =
+    if filter ref env typ then plain_display ans ref env typ
+  in
+  let () = generic_search iter in
+  format_display !ans
 
-let search_pattern pat inout =
-  text_pattern_search (filter_by_module_from_list inout &&&&& filter_blacklist) pat
+(** Search *)
 
-let gen_filtered_search filter_function display_function =
-  gen_crible None
-    (fun s a c -> if filter_function s a c then display_function s a c)
+let search_by_head = search_pattern
+(** Now search_by_head is the same as search_pattern... *)
 
 (** SearchAbout *)
 
+let name_of_reference ref = Id.to_string (basename_of_global ref)
+
 type glob_search_about_item =
   | GlobSearchSubPattern of constr_pattern
   | GlobSearchString of string
 
 let search_about_item (itemref,typ) = function
-  | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ
-  | GlobSearchString s -> String.string_contains ~where:(name_of_reference itemref) ~what:s
-
-let raw_search_about filter_modules display_function l =
-  let filter ref' env typ =
-    filter_modules ref' env typ &&
-    List.for_all (fun (b,i) -> (b : bool) == search_about_item (ref',typ) i) l &&
-      filter_blacklist ref' () ()
-  in
-  gen_filtered_search filter display_function
+  | GlobSearchSubPattern pat ->
+    Matching.is_matching_appsubterm ~closed:false pat typ
+  | GlobSearchString s ->
+    String.string_contains ~where:(name_of_reference itemref) ~what:s
 
-let search_about reference inout =
+let search_about items mods =
   let ans = ref [] in
-  raw_search_about (filter_by_module_from_list inout) (plain_display ans) reference;
+  let filter ref env typ =
+    let eqb b1 b2 = if b1 then b2 else not b2 in
+    let f_module = module_filter mods ref env typ in
+    let f_about (b, i) = eqb b (search_about_item (ref, typ) i) in
+    let f_blacklist = blacklist_filter ref env typ in
+    f_module && List.for_all f_about items && f_blacklist
+  in
+  let iter ref env typ =
+    if filter ref env typ then plain_display ans ref env typ
+  in
+  let () = generic_search iter in
   format_display !ans
 
 let interface_search flags =
@@ -309,7 +266,7 @@ let interface_search flags =
       toggle (Libnames.is_dirpath_prefix_of mdl path) flag
     in
     let in_blacklist =
-      blacklist || (filter_blacklist ref env constr)
+      blacklist || (blacklist_filter ref env constr)
     in
     List.for_all match_name name &&
     List.for_all match_type tpe &&
@@ -340,5 +297,8 @@ let interface_search flags =
     } in
     ans := answer :: !ans;
   in
-  let () = gen_filtered_search filter_function print_function in
+  let iter ref env typ =
+    if filter_function ref env typ then print_function ref env typ
+  in
+  let () = generic_search iter in
   !ans
diff --git a/toplevel/search.mli b/toplevel/search.mli
index dce553c9f9..301f89acb7 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -23,26 +23,25 @@ type glob_search_about_item =
 type filter_function = global_reference -> env -> constr -> bool
 type display_function = global_reference -> env -> constr -> unit
 
-val search_by_head : constr -> DirPath.t list * bool -> std_ppcmds
-val search_rewrite : constr -> DirPath.t list * bool -> std_ppcmds
-val search_pattern : constr -> DirPath.t list * bool -> std_ppcmds
-val search_about  :
-  (bool * glob_search_about_item) list -> DirPath.t list * bool -> std_ppcmds
+(** {6 Generic filter functions} *)
 
-val interface_search : (Interface.search_constraint * bool) list ->
-  string Interface.coq_object list
+val blacklist_filter : filter_function
+(** Check whether a reference is blacklisted. *)
+
+val module_filter : DirPath.t list * bool -> filter_function
+(** Check whether a reference pertains or not to a set of modules *)
 
-(** The filtering function that is by standard search facilities.
-   It can be passed as argument to the raw search functions. *)
+(** {6 Specialized search functions} *)
 
-val filter_by_module_from_list : DirPath.t list * bool -> filter_function
+val search_by_head : constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_rewrite : constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_pattern : constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_about   : (bool * glob_search_about_item) list ->
+  DirPath.t list * bool -> std_ppcmds
+val interface_search : (Interface.search_constraint * bool) list ->
+  string Interface.coq_object list
 
-val filter_blacklist : filter_function
+(** {6 Generic search function} *)
 
-(** raw search functions can be used for various extensions. *)
-val gen_filtered_search : filter_function -> display_function -> unit
-val filtered_search : filter_function -> display_function -> global_reference -> unit
-val raw_pattern_search : filter_function -> display_function -> constr_pattern -> unit
-val raw_search_rewrite : filter_function -> display_function -> constr_pattern -> unit
-val raw_search_about : filter_function -> display_function -> (bool * glob_search_about_item) list -> unit
-val raw_search_by_head : filter_function -> display_function -> constr_pattern -> unit
+val generic_search : display_function -> unit
+(** This function iterates over all known declarations *)
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 56c79eddac..a3da105aed 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -4,7 +4,6 @@ Class
 Locality
 Metasyntax
 Auto_ind_decl
-Libtypes
 Search
 Autoinstance
 Lemmas
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7877d9951b..9329ab9ff3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1444,16 +1444,15 @@ let interp_search_about_item = function
 
 let vernac_search s r =
   let r = interp_search_restriction r in
+  let env = Global.env () in
+  let get_pattern c = snd (Constrintern.intern_constr_pattern Evd.empty env c) in
   match s with
   | SearchPattern c ->
-      let (_,c) = interp_open_constr_patvar Evd.empty (Global.env()) c in
-      msg_notice (Search.search_pattern c r)
+      msg_notice (Search.search_pattern (get_pattern c) r)
   | SearchRewrite c ->
-      let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
-      msg_notice (Search.search_rewrite pat r)
+      msg_notice (Search.search_rewrite (get_pattern c) r)
   | SearchHead c ->
-      let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
-      msg_notice (Search.search_by_head pat r)
+      msg_notice (Search.search_by_head (get_pattern c) r)
   | SearchAbout sl ->
       msg_notice (Search.search_about (List.map (on_snd interp_search_about_item) sl) r)