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

11 files changed, 50 insertions, 39 deletions

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index cada4f3fca..f82cb64179 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -147,8 +147,8 @@ let (theory_to_obj, obj_to_theory) =
   let cache_th (_,(c, th)) = theories_map_add (c,th)
   and spec_th x = x in
   declare_object ("tactic-ring-theory",
-		  { load_function = cache_th;
-		    open_function = (fun _ -> ());
+		  { load_function = (fun _ -> ());
+		    open_function = cache_th;
                     cache_function = cache_th;
 		    specification_function = spec_th })
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 92074d7b93..ad0b844bed 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -82,7 +82,6 @@ module MakeTable =
     let (add_option,remove_option) =
       if A.synchronous then
         let load_options _ = () in
-	let open_options _ = () in
         let cache_options (_,(f,p)) = match f with
           | GOadd -> t := MySet.add p !t
           | GOrmv -> t := MySet.remove p !t in
@@ -90,7 +89,7 @@ module MakeTable =
         let (inGo,outGo) =
           Libobject.declare_object (kn,
               { Libobject.load_function = load_options;
-		Libobject.open_function = open_options;
+		Libobject.open_function = cache_options;
 		Libobject.cache_function = cache_options;
 		Libobject.specification_function = specification_options}) in
         ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
@@ -203,14 +202,13 @@ let async_value_tab = ref OptionMap.empty
 (* Tools for synchronous options *)
 
 let load_sync_value _ = ()
-let open_sync_value _ = ()
 let cache_sync_value (_,(k,v)) =
   sync_value_tab := OptionMap.add k v !sync_value_tab
 let spec_sync_value fp = fp
 let (inOptVal,_) =
    Libobject.declare_object ("Sync_option_value",
      {Libobject.load_function = load_sync_value;
-      Libobject.open_function = open_sync_value;
+      Libobject.open_function = cache_sync_value;
       Libobject.cache_function = cache_sync_value;
       Libobject.specification_function = spec_sync_value})
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 249633cbdf..b4274e9fe9 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 9efd881fac..b3b0af4634 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 606e8d9861..736a2be67f 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)
diff --git a/proofs/macros.ml b/proofs/macros.ml
index 95da5702d5..92cc8cf41c 100644
--- a/proofs/macros.ml
+++ b/proofs/macros.ml
@@ -43,7 +43,7 @@ let (inMD,outMD) =
   declare_object ("TACTIC-MACRO-DATA",
                   { cache_function = cache_md;
 		    load_function = (fun _ -> ());
-                    open_function = (fun _ -> ());
+                    open_function = cache_md;
                     specification_function = specification_md })
 
 let add_macro_hint na (ids,body) =
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 22905459f5..72593da368 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -945,8 +945,8 @@ let (inMD,outMD) =
     in add (na,ve) in 
     declare_object ("TACTIC-DEFINITION",
        {cache_function         = cache_md;
-        load_function          = cache_md;
-        open_function          = (fun _ -> ());
+        load_function          = (fun _ -> ());
+        open_function          = cache_md;
         specification_function = (fun x -> x)})
 
 (* Adds a Tactic Definition in the table *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index a2a56fa9a0..32c256ad35 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -167,9 +167,9 @@ let specification_autohint x = x
 
 let (inAutoHint,outAutoHint) =
   declare_object ("AUTOHINT",
-                  { load_function = cache_autohint;
+                  { load_function = (fun _ -> ());
                     cache_function = cache_autohint;
-		    open_function = (fun _ -> ());
+		    open_function = cache_autohint;
                     specification_function = specification_autohint })
 
 (**************************************************************************)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 42529c56a7..938ead22f0 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -196,7 +196,7 @@ let ((inDD : destructor_data_object->obj),
   declare_object ("DESTRUCT-HYP-CONCL-DATA",
                   { load_function = (fun _ -> ());
                     cache_function = cache_dd;
-		    open_function = (fun _ -> ());
+		    open_function = cache_dd;
                     specification_function = specification_dd })
     
 let add_destructor_hint na pat pri code =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6d4bc8d55a..3943cc07e4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1582,7 +1582,6 @@ let rules_of_base rbase = List.rev (Gmapl.find rbase !rew_tab)
 
 (*Functions necessary to the library object declaration*)
 let load_autorewrite_rule _ = ()
-let open_autorewrite_rule _ = ()
 let cache_autorewrite_rule (_,(rbase,lrl)) = add_list_rules rbase lrl
 let specification_autorewrite_rule x = x
 
@@ -1591,7 +1590,7 @@ let (in_autorewrite_rule,out_autorewrite_rule)=
   Libobject.declare_object
     ("AUTOREWRITE_RULE",
      { Libobject.load_function = load_autorewrite_rule;
-       Libobject.open_function = open_autorewrite_rule;
+       Libobject.open_function = cache_autorewrite_rule;
        Libobject.cache_function = cache_autorewrite_rule;
        Libobject.specification_function = specification_autorewrite_rule })
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e0ccdc6e4d..78481ca1e7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -41,12 +41,14 @@ let _ =
       init_function = Esyntax.init }
 
 (* Pretty-printing objects = syntax_entry *)
+let cache_syntax (_,ppobj) = Esyntax.add_ppobject ppobj
+
 let (inPPSyntax,outPPSyntax) =
   declare_object
     ("PPSYNTAX",
-     { load_function = (fun (_,ppobj) -> Esyntax.add_ppobject ppobj);
-       open_function = (fun _ -> ());
-       cache_function = (fun (_,ppobj) -> Esyntax.add_ppobject ppobj);
+     { load_function = (fun _ -> ());
+       open_function = cache_syntax;
+       cache_function = cache_syntax;
        specification_function = (fun x -> x) })
 
 (* Syntax extension functions (registered in the environnement) *)
@@ -71,23 +73,27 @@ let _ =
 
 (* Tokens *)
 
+let cache_token (_,s) = Pcoq.lexer.Token.using ("", s)
+
 let (inToken, outToken) =
   declare_object
     ("TOKEN",
      { load_function = (fun _ -> ());
-       open_function = (fun _ -> ());
-       cache_function = (fun (_, s) -> Pcoq.lexer.Token.using ("", s));
+       open_function = cache_token;
+       cache_function = cache_token;
        specification_function = (fun x -> x)})
 
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
 (* Grammar rules *)
+let cache_grammar (_,a) = Egrammar.extend_grammar a
+
 let (inGrammar, outGrammar) =
   declare_object
     ("GRAMMAR",
-     { load_function = (fun (_, a) -> Egrammar.extend_grammar a);
-       open_function = (fun _ -> ());
-       cache_function = (fun (_, a) -> Egrammar.extend_grammar a);
+     { load_function = (fun _ -> ());
+       open_function = cache_grammar;
+       cache_function = cache_grammar;
        specification_function = (fun x -> x)})
 
 let add_grammar_obj univ al =
@@ -130,8 +136,8 @@ let cache_infix (_,(gr,se)) =
 let (inInfix, outInfix) =
   declare_object
     ("INFIX",
-     { load_function = cache_infix;
-       open_function = (fun _ -> ());
+     { load_function = (fun _ -> ());
+       open_function = cache_infix;
        cache_function = cache_infix;
        specification_function = (fun x -> x)})