diff options
Diffstat (limited to 'toplevel/libtypes.ml')
| -rw-r--r-- | toplevel/libtypes.ml | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index c999c0609..fa636989a 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -10,21 +10,21 @@ open Term open Summary open Libobject -(* +(* * Module construction *) - -let reduce c = Reductionops.head_unfold_under_prod + +let reduce c = Reductionops.head_unfold_under_prod (Auto.Hint_db.transparent_state (Auto.searchtable_map "typeclass_instances")) (Global.env()) Evd.empty c -module TypeDnet = Term_dnet.Make(struct +module TypeDnet = Term_dnet.Make(struct type t = Libnames.global_reference let compare = Pervasives.compare let subst s gr = fst (Libnames.subst_global s gr) let constr_of = Global.type_of_global end) - (struct let reduce = reduce + (struct let reduce = reduce let direction = false end) type result = Libnames.global_reference * (constr*existential_key) * Termops.subst @@ -36,18 +36,18 @@ let defined_types = ref TypeDnet.empty * Bookeeping & States *) -let freeze () = +let freeze () = (!all_types,!defined_types) -let unfreeze (lt,dt) = - all_types := lt; +let unfreeze (lt,dt) = + all_types := lt; defined_types := dt -let init () = - all_types := TypeDnet.empty; +let init () = + all_types := TypeDnet.empty; defined_types := TypeDnet.empty -let _ = +let _ = declare_summary "type-library-state" { freeze_function = freeze; unfreeze_function = unfreeze; @@ -56,7 +56,7 @@ let _ = let load (_,d) = (* Profile.print_logical_stats !all_types; Profile.print_logical_stats d;*) - all_types := TypeDnet.union d !all_types + all_types := TypeDnet.union d !all_types let subst s t = TypeDnet.subst s t (* @@ -66,18 +66,18 @@ 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,output) = +let (input,output) = declare_object { (default_object "LIBTYPES") with load_function = (fun _ -> load); subst_function = (fun (_,s,t) -> subst s t); export_function = (fun x -> Some x); - classify_function = (fun x -> Substitute x) + classify_function = (fun x -> Substitute x) } let update () = Lib.add_anonymous_leaf (input !defined_types) -(* +(* * Search interface *) @@ -93,12 +93,12 @@ let add typ gr = let add_key = Profile.declare_profile "add" let add a b = Profile.profile1 add_key add a b *) - -(* - * Hooks declaration + +(* + * Hooks declaration *) -let _ = Declare.add_cache_hook +let _ = Declare.add_cache_hook ( fun sp -> let gr = Nametab.global_of_path sp in let ty = Global.type_of_global gr in |