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

1 files changed, 0 insertions, 110 deletions

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