Bugs lies a la confusion load/open et a un open abusivement recursif dans library

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@839 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 23 insertions, 15 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 249633cbd..b4274e9fe 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -166,11 +166,13 @@ let lookup_path_to_sort_from s =
 (*val inClass : (cl_typ * cl_info_typ) -> Libobject.object = <fun>
  val outClass : Libobject.object -> (cl_typ * cl_info_typ) = <fun> *)
 
+let cache_class (_,x) = add_new_class1 x
+
 let (inClass,outClass) =
   declare_object ("CLASS",
-                  { load_function = (function  (_,x) -> add_new_class1 x);
-		    open_function = (fun _ -> ());
-                    cache_function = (function  (_,x) -> add_new_class1 x);
+                  { load_function = (fun _ -> ());
+		    open_function = cache_class;
+                    cache_function = cache_class;
                     specification_function = (function x -> x) })
 
 let add_new_class (cl,s,stre,p) = 
@@ -315,11 +317,11 @@ let add_new_coercion_in_graph ((coef,xf),cls,clt) =
    val outCoercion : Libobject.object -> (coe_typ * coe_info_typ) 
                          * cl_typ * cl_typ *)
 
+let cache_coercion (_,x) = add_new_coercion_in_graph x
+
 let (inCoercion,outCoercion) =
   declare_object ("COERCION",
                   { load_function = (fun _ -> ());
-		    open_function =
-                      (function  (_,x) -> add_new_coercion_in_graph x);
-                    cache_function =
-                      (function  (_,x) -> add_new_coercion_in_graph x);
+		    open_function = cache_coercion;
+                    cache_function = cache_coercion;
                     specification_function = (function x -> x) })
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 9efd881fa..b3b0af463 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -31,11 +31,13 @@ let sTRUCS = (ref [] : (inductive_path * struc_typ) list ref)
 
 let add_new_struc1 x = sTRUCS:=x::(!sTRUCS)
 
+let cache_structure (_,x) = add_new_struc1 x
+
 let (inStruc,outStruc) =
   declare_object ("STRUCTURE",
                   { load_function = (fun _ -> ());
-                    cache_function = (function  (_,x) -> add_new_struc1 x);
-		    open_function = (fun _ -> ());
+                    cache_function = cache_structure;
+		    open_function = cache_structure;
                     specification_function = (function x -> x) })
 
 let add_new_struc (s,c,n,l) = 
@@ -63,11 +65,13 @@ let oBJDEFS = (ref [] : ((cte_typ * cte_typ) * obj_typ) list ref)
 
 let add_new_objdef1 x = oBJDEFS:=x::(!oBJDEFS)
 
+let cache_obj (_,x) = add_new_objdef1 x
+
 let (inObjDef,outObjDef) =
   declare_object ("OBJDEF",
                   { load_function = (fun _ -> ());
-		    open_function = (fun _ -> ());
-                    cache_function = (function  (_,x) -> add_new_objdef1 x);
+		    open_function = cache_obj;
+                    cache_function = cache_obj;
                     specification_function = (function x -> x)})
 
 let add_new_objdef (o,c,la,lp,l) =
@@ -77,11 +81,13 @@ let add_new_objdef (o,c,la,lp,l) =
     Lib.add_anonymous_leaf
       (inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l}))
 
+let cache_objdef1 (_,sp) = ()
+
 let ((inObjDef1 : section_path -> obj),(outObjDef1 : obj -> section_path)) =
   declare_object ("OBJDEF1",
                   { load_function = (fun _ -> ());
-		    open_function = (fun _ -> ());
-                    cache_function = (function  (_,sp) -> ());
+		    open_function = cache_objdef1;
+                    cache_function = cache_objdef1;
                     specification_function = (function x -> x)})
 
 let objdef_info o = List.assoc o !oBJDEFS
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 606e8d986..736a2be67 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -29,8 +29,8 @@ let open_syntax_constant (sp,_) =
 let (in_syntax_constant, out_syntax_constant) =
   let od = {
     cache_function = cache_syntax_constant;
-    load_function = cache_syntax_constant;
-    open_function = (fun _ -> ());
+    load_function = (fun _ -> ());
+    open_function = cache_syntax_constant;
     specification_function = (fun x -> x) } 
   in
   declare_object ("SYNTAXCONSTANT", od)