methode export

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

17 files changed, 60 insertions, 55 deletions

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index f82cb6417..2a817668e 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -145,12 +145,12 @@ let _ =
 
 let (theory_to_obj, obj_to_theory) = 
   let cache_th (_,(c, th)) = theories_map_add (c,th)
-  and spec_th x = x in
+  and export_th x = Some x in
   declare_object ("tactic-ring-theory",
 		  { load_function = (fun _ -> ());
 		    open_function = cache_th;
                     cache_function = cache_th;
-		    specification_function = spec_th })
+		    export_function = export_th })
 
 (* from the set A, guess the associated theory *)
 (* With this simple solution, the theory to use is automatically guessed *)
diff --git a/library/declare.ml b/library/declare.ml
index 49d684ed6..72f16f48f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -67,14 +67,14 @@ let load_variable _ = ()
 
 let open_variable _ = ()
 
-let specification_variable x = x
+let export_variable x = None
 
 let (in_variable, out_variable) =
   let od = {
     cache_function = cache_variable;
     load_function = load_variable;
     open_function = open_variable;
-    specification_function = specification_variable } in
+    export_function = export_variable } in
   declare_object ("VARIABLE", od)
 
 let out_variable sp = fst (out_variable sp)
@@ -96,14 +96,14 @@ let load_parameter (sp,(_,imps)) =
 let open_parameter (sp,_) =
   Nametab.push (basename sp) sp
 
-let specification_parameter obj = obj
+let export_parameter obj = Some obj
 
 let (in_parameter, out_parameter) =
   let od = {
     cache_function = cache_parameter;
     load_function = load_parameter;
     open_function = open_parameter;
-    specification_function = specification_parameter } 
+    export_function = export_parameter } 
   in
   declare_object ("PARAMETER", od)
 
@@ -141,14 +141,14 @@ let load_constant (sp,((ce,stre),imps)) =
 let open_constant (sp,_) =
   Nametab.push (basename sp) sp
 
-let specification_constant obj = obj
+let export_constant obj = Some obj
 
 let (in_constant, out_constant) =
   let od = {
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
-    specification_function = specification_constant } 
+    export_function = export_constant } 
   in
   declare_object ("CONSTANT", od)
 
@@ -176,14 +176,14 @@ let load_inductive (sp,(_,imps)) =
 let open_inductive (sp,(mie,_)) =
   push_inductive_names sp mie
 
-let specification_inductive obj = obj
+let export_inductive obj = Some obj
 
 let (in_inductive, out_inductive) =
   let od = {
     cache_function = cache_inductive;
     load_function = load_inductive;
     open_function = open_inductive;
-    specification_function = specification_inductive } 
+    export_function = export_inductive } 
   in
   declare_object ("INDUCTIVE", od)
 
diff --git a/library/goptions.ml b/library/goptions.ml
index ad0b844be..64b08f6f4 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -85,13 +85,13 @@ module MakeTable =
         let cache_options (_,(f,p)) = match f with
           | GOadd -> t := MySet.add p !t
           | GOrmv -> t := MySet.remove p !t in
-        let specification_options fp = fp in
+        let export_options fp = Some fp in
         let (inGo,outGo) =
           Libobject.declare_object (kn,
               { Libobject.load_function = load_options;
 		Libobject.open_function = cache_options;
 		Libobject.cache_function = cache_options;
-		Libobject.specification_function = specification_options}) in
+		Libobject.export_function = export_options}) in
         ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
          (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
       else
@@ -204,13 +204,13 @@ let async_value_tab = ref OptionMap.empty
 let load_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 export_sync_value fp = Some fp
 let (inOptVal,_) =
-   Libobject.declare_object ("Sync_option_value",
-     {Libobject.load_function = load_sync_value;
+  Libobject.declare_object ("Sync_option_value",
+    { Libobject.load_function = load_sync_value;
       Libobject.open_function = cache_sync_value;
       Libobject.cache_function = cache_sync_value;
-      Libobject.specification_function = spec_sync_value})
+      Libobject.export_function = export_sync_value })
 
 let freeze_sync_table () = !sync_value_tab
 let unfreeze_sync_table l = sync_value_tab := l
diff --git a/library/impargs.ml b/library/impargs.ml
index b479dc5b9..c9fa33e24 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -123,7 +123,7 @@ let is_implicit_inductive_definition sp =
 let is_implicit_var id =
   try let _ = Idmap.find id !var_table in true with Not_found -> false
 
-(* Registration as global tables and roolback. *)
+(* Registration as global tables and rollback. *)
 
 type frozen_t = bool
               * implicits Spmap.t 
diff --git a/library/lib.ml b/library/lib.ml
index 74986d6fe..3a502d42e 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -151,12 +151,15 @@ let close_section s =
 let export_module () =
   if !module_name = None then error "no module declared";
   let rec clean acc = function
-    | (_,Module _) :: _ -> acc
-    | (_,Leaf _) as node :: stk -> clean (node::acc) stk
-    | (_,ClosedSection _) as node :: stk -> clean (node::acc) stk
+    | (_,Module _) :: _ | [] -> acc
+    | (sp,Leaf o) as node :: stk -> 
+	(match export_object o with 
+	   | None -> clean acc stk
+	   | Some o' -> clean ((sp,Leaf o') :: acc) stk)
+    | (sp,ClosedSection (s,ctx)) :: stk -> 
+	clean ((sp,ClosedSection (s, clean [] ctx)) :: acc) stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
     | (_,FrozenState _) :: stk -> clean acc stk
-    | _ -> assert false
   in
   clean [] !lib_stk
 
diff --git a/library/libobject.ml b/library/libobject.ml
index 1eb7aea0e..c644cc4eb 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -8,7 +8,7 @@ type 'a object_declaration = {
   cache_function : section_path * 'a -> unit;
   load_function : section_path * 'a -> unit;
   open_function : section_path * 'a -> unit;
-  specification_function : 'a -> 'a }
+  export_function : 'a -> 'a option }
 
 type obj = Dyn.t (* persistent dynamic objects *)
 
@@ -16,7 +16,7 @@ type dynamic_object_declaration = {
   dyn_cache_function : section_path * obj -> unit;
   dyn_load_function : section_path * obj -> unit;
   dyn_open_function : section_path * obj -> unit;
-  dyn_specification_function : obj -> obj }
+  dyn_export_function : obj -> obj option }
 
 let object_tag lobj = Dyn.tag lobj
 
@@ -34,13 +34,13 @@ let declare_object (na,odecl) =
   and opener (spopt,lobj) =
     if Dyn.tag lobj = na then odecl.open_function (spopt,outfun lobj)
     else anomaly "somehow we got the wrong dynamic object in the openfun"
-  and spec_extractor lobj = 
-    infun(odecl.specification_function (outfun lobj))
+  and exporter lobj = 
+    option_app infun (odecl.export_function (outfun lobj))
   in 
   Hashtbl.add cache_tab na { dyn_cache_function = cacher;
 			     dyn_load_function = loader;
                              dyn_open_function = opener;
-                             dyn_specification_function = spec_extractor };
+                             dyn_export_function = exporter };
   (infun,outfun)
 
 let apply_dyn_fun f lobj =
@@ -50,7 +50,8 @@ let apply_dyn_fun f lobj =
       Hashtbl.find cache_tab tag
     with Not_found -> 
       anomaly ("Cannot find library functions for an object with tag "^tag)
-  in f dodecl
+  in 
+  f dodecl
 
 let cache_object ((_,lobj) as node) =
   apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj
@@ -61,5 +62,5 @@ let load_object ((_,lobj) as node) =
 let open_object ((_,lobj) as node) = 
   apply_dyn_fun (fun d -> d.dyn_open_function node) lobj
 
-let extract_object_specification lobj =
-  apply_dyn_fun (fun d -> d.dyn_specification_function lobj) lobj
+let export_object lobj =
+  apply_dyn_fun (fun d -> d.dyn_export_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index d855059fa..17a221a66 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -19,7 +19,7 @@ type 'a object_declaration = {
   cache_function : section_path * 'a -> unit;
   load_function : section_path * 'a -> unit;
   open_function : section_path * 'a -> unit;
-  specification_function : 'a -> 'a }
+  export_function : 'a -> 'a option }
 
 (*s Given an object name and a declaration, the function [declare_object]
    will hand back two functions, the "injection" and "projection"
@@ -35,4 +35,5 @@ val object_tag : obj -> string
 val cache_object : section_path * obj -> unit
 val load_object : section_path * obj -> unit
 val open_object : section_path * obj -> unit
-val extract_object_specification : obj -> obj
+val export_object : obj -> obj option
+
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b4274e9fe..306f2b8ce 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -173,7 +173,7 @@ let (inClass,outClass) =
                   { load_function = (fun _ -> ());
 		    open_function = cache_class;
                     cache_function = cache_class;
-                    specification_function = (function x -> x) })
+                    export_function = (function x -> Some x) })
 
 let add_new_class (cl,s,stre,p) = 
   Lib.add_anonymous_leaf (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})))
@@ -324,4 +324,4 @@ let (inCoercion,outCoercion) =
                   { load_function = (fun _ -> ());
 		    open_function = cache_coercion;
                     cache_function = cache_coercion;
-                    specification_function = (function x -> x) })
+                    export_function = (function x -> Some x) })
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b3b0af463..45b16c935 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -38,7 +38,7 @@ let (inStruc,outStruc) =
                   { load_function = (fun _ -> ());
                     cache_function = cache_structure;
 		    open_function = cache_structure;
-                    specification_function = (function x -> x) })
+                    export_function = (function x -> Some x) })
 
 let add_new_struc (s,c,n,l) = 
   Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
@@ -72,7 +72,7 @@ let (inObjDef,outObjDef) =
                   { load_function = (fun _ -> ());
 		    open_function = cache_obj;
                     cache_function = cache_obj;
-                    specification_function = (function x -> x)})
+                    export_function = (function x -> Some x)})
 
 let add_new_objdef (o,c,la,lp,l) =
   try 
@@ -88,7 +88,7 @@ let ((inObjDef1 : section_path -> obj),(outObjDef1 : obj -> section_path)) =
                   { load_function = (fun _ -> ());
 		    open_function = cache_objdef1;
                     cache_function = cache_objdef1;
-                    specification_function = (function x -> x)})
+                    export_function = (function x -> Some x)})
 
 let objdef_info o = List.assoc o !oBJDEFS
 
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 736a2be67..00ed971c1 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -31,7 +31,7 @@ let (in_syntax_constant, out_syntax_constant) =
     cache_function = cache_syntax_constant;
     load_function = (fun _ -> ());
     open_function = cache_syntax_constant;
-    specification_function = (fun x -> x) } 
+    export_function = (fun x -> Some x) } 
   in
   declare_object ("SYNTAXCONSTANT", od)
 
diff --git a/proofs/macros.ml b/proofs/macros.ml
index 92cc8cf41..4a7a826f9 100644
--- a/proofs/macros.ml
+++ b/proofs/macros.ml
@@ -39,12 +39,12 @@ let _ =
 let (inMD,outMD) =
   let add (na,md) = mactab := Stringmap.add na md !mactab in
   let cache_md (_,(na,md)) = add (na,md) in 
-  let specification_md x = x in
+  let export_md x = Some x in
   declare_object ("TACTIC-MACRO-DATA",
                   { cache_function = cache_md;
 		    load_function = (fun _ -> ());
                     open_function = cache_md;
-                    specification_function = specification_md })
+                    export_function = export_md })
 
 let add_macro_hint na (ids,body) =
   if Stringmap.mem na !mactab then errorlabstrm "add_macro_hint"
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 72593da36..f45d896d4 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -944,10 +944,10 @@ let (inMD,outMD) =
     let ve=val_interp (Evd.empty,Environ.empty_env,[],[],None,get_debug ()) td 
     in add (na,ve) in 
     declare_object ("TACTIC-DEFINITION",
-       {cache_function         = cache_md;
-        load_function          = (fun _ -> ());
-        open_function          = cache_md;
-        specification_function = (fun x -> x)})
+       {cache_function  = cache_md;
+        load_function   = (fun _ -> ());
+        open_function   = cache_md;
+        export_function = (fun x -> Some x)})
 
 (* Adds a Tactic Definition in the table *)
 let add_tacdef na vbody =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 32c256ad3..10de3ab49 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -163,14 +163,14 @@ let add_hint dbname hintlist =
 let cache_autohint (_,(name,hintlist)) =
   try add_hint name hintlist with _ -> anomaly "Auto.add_hint"
 
-let specification_autohint x = x
+let export_autohint x = Some x
 
 let (inAutoHint,outAutoHint) =
   declare_object ("AUTOHINT",
                   { load_function = (fun _ -> ());
                     cache_function = cache_autohint;
 		    open_function = cache_autohint;
-                    specification_function = specification_autohint })
+                    export_function = export_autohint })
 
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 938ead22f..628c337f9 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -187,7 +187,7 @@ let cache_dd (_,(na,dd)) =
       [< 'sTR"The code which adds destructor hints broke;"; 'sPC; 
 	 'sTR"this is not supposed to happen" >]
 
-let specification_dd x = x
+let export_dd x = Some x
 
 type destructor_data_object = identifier * destructor_data
 
@@ -197,7 +197,7 @@ let ((inDD : destructor_data_object->obj),
                   { load_function = (fun _ -> ());
                     cache_function = cache_dd;
 		    open_function = cache_dd;
-                    specification_function = specification_dd })
+                    export_function = export_dd })
     
 let add_destructor_hint na pat pri code =
   Lib.add_anonymous_leaf
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3943cc07e..6d1cc5a69 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1583,7 +1583,7 @@ let rules_of_base rbase = List.rev (Gmapl.find rbase !rew_tab)
 (*Functions necessary to the library object declaration*)
 let load_autorewrite_rule _ = ()
 let cache_autorewrite_rule (_,(rbase,lrl)) = add_list_rules rbase lrl
-let specification_autorewrite_rule x = x
+let export_autorewrite_rule x = Some x
 
 (*Declaration of the AUTOREWRITE_RULE library object*)
 let (in_autorewrite_rule,out_autorewrite_rule)=
@@ -1592,7 +1592,7 @@ let (in_autorewrite_rule,out_autorewrite_rule)=
      { Libobject.load_function = load_autorewrite_rule;
        Libobject.open_function = cache_autorewrite_rule;
        Libobject.cache_function = cache_autorewrite_rule;
-       Libobject.specification_function = specification_autorewrite_rule })
+       Libobject.export_function = export_autorewrite_rule })
 
 (* Semantic of the HintRewrite vernacular command *)
 let _ = 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 78481ca1e..4a4c92531 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -49,7 +49,7 @@ let (inPPSyntax,outPPSyntax) =
      { load_function = (fun _ -> ());
        open_function = cache_syntax;
        cache_function = cache_syntax;
-       specification_function = (fun x -> x) })
+       export_function = (fun x -> Some x) })
 
 (* Syntax extension functions (registered in the environnement) *)
 
@@ -81,7 +81,7 @@ let (inToken, outToken) =
      { load_function = (fun _ -> ());
        open_function = cache_token;
        cache_function = cache_token;
-       specification_function = (fun x -> x)})
+       export_function = (fun x -> Some x)})
 
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
@@ -94,7 +94,7 @@ let (inGrammar, outGrammar) =
      { load_function = (fun _ -> ());
        open_function = cache_grammar;
        cache_function = cache_grammar;
-       specification_function = (fun x -> x)})
+       export_function = (fun x -> Some x)})
 
 let add_grammar_obj univ al =
    Lib.add_anonymous_leaf (inGrammar (Extend.interp_grammar_command univ al))
@@ -139,7 +139,7 @@ let (inInfix, outInfix) =
      { load_function = (fun _ -> ());
        open_function = cache_infix;
        cache_function = cache_infix;
-       specification_function = (fun x -> x)})
+       export_function = (fun x -> Some x)})
 
 let prec_assoc = function
   | Some(Gramext.RightA) -> (":L",":E")
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 66577bea6..7d0761771 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -221,14 +221,14 @@ let cache_ml_module_object (_,{mnames=mnames}) =
          add_loaded_module mname)
     mnames
 
-let specification_ml_module_object x = x
+let export_ml_module_object x = Some x
 					 
 let (inMLModule,outMLModule) =
   declare_object ("ML-MODULE",
                   { load_function = cache_ml_module_object;
                     cache_function = cache_ml_module_object;
 		    open_function = (fun _ -> ());
-                    specification_function = specification_ml_module_object })
+                    export_function = export_ml_module_object })
 
 let declare_ml_modules l =
   Lib.add_anonymous_leaf (inMLModule {mnames=l})