4 files changed, 23 insertions, 8 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 0fc9772da9..2a4b2e4031 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -39,6 +39,9 @@ let set_xml_declare_variable f = xml_declare_variable := if_xml f
 let set_xml_declare_constant f = xml_declare_constant := if_xml f
 let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
 
+let cache_hook = ref ignore
+let add_cache_hook f = cache_hook := f
+
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
@@ -87,6 +90,7 @@ let declare_variable id obj =
   !xml_declare_variable oname;
   oname
 
+
 (** Declaration of constants and parameters *)
 
 type constant_declaration = constant_entry * logical_kind
@@ -114,7 +118,8 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   add_section_constant kn' (Global.lookup_constant kn').const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  add_constant_kind (constant_of_kn kn) kind
+  add_constant_kind (constant_of_kn kn) kind;
+  !cache_hook sp
 
 let discharged_hyps kn sechyps =
   let (_,dir,_) = repr_kn kn in
@@ -160,11 +165,11 @@ let hcons_constant_declaration = function
 
 let declare_constant_common id dhyps (cd,kind) =
   let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in
-  let kn = constant_of_kn kn in
-  declare_constant_implicits kn;
-  Heads.declare_head (EvalConstRef kn);
-  Notation.declare_ref_arguments_scope (ConstRef kn);
-  kn
+  let c = constant_of_kn kn in
+  declare_constant_implicits c;
+  Heads.declare_head (EvalConstRef c);
+  Notation.declare_ref_arguments_scope (ConstRef c);
+  c
 
 let declare_constant_gen internal id (cd,kind) =
   let cd = hcons_constant_declaration cd in
@@ -215,7 +220,7 @@ let check_exists_inductive (sp,_) =
 let load_inductive i ((sp,kn),(_,mie)) =
   let names = inductive_names sp kn mie in
   List.iter check_exists_inductive names;
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
 
 let open_inductive i ((sp,kn),(_,mie)) =
   let names = inductive_names sp kn mie in
@@ -230,7 +235,9 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   assert (kn'=kn);
   add_section_kn kn (Global.lookup_mind kn').mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names;
+  List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie)
+
 
 let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let mie = Global.lookup_mind kn in
diff --git a/library/declare.mli b/library/declare.mli
index 93c8b9f919..38b1fa7b2e 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -63,3 +63,6 @@ val declare_mind : bool -> mutual_inductive_entry -> object_name
 val set_xml_declare_variable : (object_name -> unit) -> unit
 val set_xml_declare_constant : (bool * constant -> unit) -> unit
 val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
+
+(* hook for the cache function of constants and inductives *)
+val add_cache_hook : (section_path -> unit) -> unit
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 76487af686..16f9c9491b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -824,8 +824,11 @@ let start_library dir =
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
+let end_library_hook = ref ignore
+let set_end_library_hook f = end_library_hook := f
 
 let end_library dir = 
+  !end_library_hook();
   let prefix, lib_stack = Lib.end_compilation dir in
   let cenv = Global.export dir in
   let msid = msid_of_prefix prefix in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 1f7f6ada0a..322078e9b8 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -82,6 +82,8 @@ val start_library : library_name -> unit
 val end_library :
   library_name -> Safe_typing.compiled_library * library_objects
 
+(* set a function to be executed at end_library *)
+val set_end_library_hook : (unit -> unit) -> unit
 
 (* [really_import_module mp] opens the module [mp] (in a Caml sense).
    It modifies Nametab and performs the [open_object] function for