methode export

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

6 files changed, 34 insertions, 29 deletions

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
+