From d06e75b5011ba29119d868e904138b5c3e2e8215 Mon Sep 17 00:00:00 2001
From: puech
Date: Wed, 28 Oct 2009 13:36:28 +0000
Subject: Fix incorrect registration of objects in libtypes.ml when defining a
 module.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12432 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/library/declare.ml b/library/declare.ml
index dd1b12a24f..cf2f1fbaec 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -101,9 +101,10 @@ let load_constant i ((sp,kn),(_,_,kind)) =
     errorlabstrm "cache_constant"
       (pr_id (basename sp) ++ str " already exists");
   let con = Global.constant_of_delta (constant_of_kn kn) in
-    Nametab.push (Nametab.Until i) sp (ConstRef con);
-    add_constant_kind con kind
-      
+  Nametab.push (Nametab.Until i) sp (ConstRef con);
+  add_constant_kind con kind;
+  !cache_hook sp
+
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
   let con = constant_of_kn kn in
@@ -219,7 +220,8 @@ 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;
+  List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie)
 
 let open_inductive i ((sp,kn),(_,mie)) =
   let names = inductive_names sp kn mie in
-- 
cgit v1.2.3