From 508e8afd8538dd38afa4eaa0dd9c7e349e50e20d Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 19 Mar 2013 15:18:03 +0000
Subject: 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
---
 toplevel/libtypes.ml | 110 ---------------------------------------------------
 1 file changed, 110 deletions(-)
 delete mode 100644 toplevel/libtypes.ml

(limited to 'toplevel/libtypes.ml')

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
-- 
cgit v1.2.3