Remove useless Liboject.export_function field

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

8 files changed, 16 insertions, 69 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 49b7d7ba2..da723aa4b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -138,8 +138,6 @@ let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false))
 
 let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
 
-let export_constant cst = Some (dummy_constant cst)
-
 let classify_constant cst = Substitute (dummy_constant cst)
 
 let (inConstant,_) =
@@ -149,8 +147,7 @@ let (inConstant,_) =
     open_function = open_constant;
     classify_function = classify_constant;
     subst_function = ident_subst_function;
-    discharge_function = discharge_constant;
-    export_function = export_constant }
+    discharge_function = discharge_constant }
 
 let hcons_constant_declaration = function
   | DefinitionEntry ce when !Flags.hash_cons_proofs ->
@@ -259,8 +256,6 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_finite = true;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
 
-let export_inductive x = Some (dummy_inductive_entry x)
-
 let (inInductive,_) =
   declare_object {(default_object "INDUCTIVE") with
     cache_function = cache_inductive;
@@ -268,8 +263,7 @@ let (inInductive,_) =
     open_function = open_inductive;
     classify_function = (fun a -> Substitute (dummy_inductive_entry a));
     subst_function = ident_subst_function;
-    discharge_function = discharge_inductive;
-    export_function = export_inductive }
+    discharge_function = discharge_inductive }
 
 (* for initial declaration *)
 let declare_mind isrecord mie =
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 37ee34d1f..d796a2906 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -296,8 +296,7 @@ let (in_module,out_module) =
     load_function = load_module;
     open_function = open_module;
     subst_function = subst_module;
-    classify_function = classify_module;
-    export_function = (fun _ -> anomaly "No modules in sections!") }
+    classify_function = classify_module }
 
 
 let rec replace_alias modalias_obj obj =
@@ -456,9 +455,7 @@ let (in_module_alias,out_module_alias) =
 		    open_function = open_module_alias;
 		    classify_function = classify_module_alias;
 		    subst_function = subst_module_alias;
-		    load_function = load_module_alias;
-		    export_function = (fun _ -> anomaly "No modules in sections!") }
-
+		    load_function = load_module_alias }
 
 
 
@@ -487,8 +484,7 @@ let (in_modkeep,_) =
   declare_object {(default_object "MODULE KEEP OBJECTS") with
     cache_function = cache_keep;
     load_function = load_keep;
-    open_function = open_keep;
-    export_function = (fun _ -> anomaly "No modules in sections!") }
+    open_function = open_keep }
 
 (* we remember objects for a module type. In case of a declaration:
    Module M:SIG:=...
@@ -572,8 +568,7 @@ let (in_modtype,_) =
       open_function = open_modtype;
       load_function = load_modtype;
       subst_function = subst_modtype;
-      classify_function = classify_modtype;
-      export_function = Option.make }
+      classify_function = classify_modtype }
 
 
 
@@ -1043,8 +1038,7 @@ let (in_include,out_include) =
     load_function = load_include;
     open_function = open_include;
     subst_function = subst_include;
-    classify_function = classify_include;
-    export_function = (fun _ -> anomaly "No modules in section!") }
+    classify_function = classify_include }
 
 let rec update_include (sub,mbids,msid,objs) =
   let rec replace_include = function
diff --git a/library/goptions.ml b/library/goptions.ml
index e4c5a6155..032016c3d 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -96,15 +96,13 @@ module MakeTable =
 	    if p' == p then obj else
 	      (f,p')
 	in
-	let export_options fp = Some fp in
         let (inGo,outGo) =
           Libobject.declare_object {(Libobject.default_object nick) with
                 Libobject.load_function = load_options;
 		Libobject.open_function = load_options;
 		Libobject.cache_function = cache_options;
 		Libobject.subst_function = subst_options;
-		Libobject.classify_function = (fun x -> Substitute x);
-		Libobject.export_function = export_options} 
+		Libobject.classify_function = (fun x -> Substitute x)}
 	in
         ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
          (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
@@ -255,9 +253,7 @@ let declare_option cast uncast
 		       cache_function = (fun (_,v) -> write v);
 		       classify_function = (fun v -> Keep v);
 		       discharge_function = (fun (_,v) -> Some v);
-		       load_function = (fun _ (_,v) -> write v);
-		       (* spiwack: I'm unsure whether this function does anyting *)
-		       export_function = (fun v -> Some v)}
+		       load_function = (fun _ (_,v) -> write v)}
     in
     let _ = declare_summary (nickname key)
 	     { freeze_function = read;
diff --git a/library/heads.ml b/library/heads.ml
index bca6b6502..150ba8942 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -155,8 +155,6 @@ let discharge_head (_,(ref,k)) =
 let rebuild_head (ref,k) =
   (ref, compute_head ref)
 
-let export_head o = Some o
-
 let (inHead, _) =
   declare_object {(default_object "HEAD") with
     cache_function = cache_head;
@@ -164,8 +162,7 @@ let (inHead, _) =
     subst_function = subst_head;
     classify_function = (fun x -> Substitute x);
     discharge_function = discharge_head;
-    rebuild_function = rebuild_head;
-    export_function = export_head }
+    rebuild_function = rebuild_head }
 
 let declare_head c =
   let hd = compute_head c in
diff --git a/library/impargs.ml b/library/impargs.ml
index edd0aba0e..d27ced220 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -521,9 +521,6 @@ let rebuild_implicits (req,l) =
 	  let l' = merge_impls auto m in [ref,l']
   in (req,l')
 
-let export_implicits (req,_ as x) =
-  if req = ImplLocal then None else Some x
-
 let (inImplicits, _) =
   declare_object {(default_object "IMPLICITS") with
     cache_function = cache_implicits;
@@ -531,8 +528,7 @@ let (inImplicits, _) =
     subst_function = subst_implicits;
     classify_function = (fun x -> Substitute x);
     discharge_function = discharge_implicits;
-    rebuild_function = rebuild_implicits;
-    export_function = export_implicits }
+    rebuild_function = rebuild_implicits }
 
 let declare_implicits_gen req flags ref =
   let imps = compute_global_implicits flags [] ref in
diff --git a/library/libobject.ml b/library/libobject.ml
index 95894294b..9beb32cfc 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -36,8 +36,7 @@ type 'a object_declaration = {
   classify_function : 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
-  rebuild_function : 'a -> 'a;
-  export_function : 'a -> 'a option }
+  rebuild_function : 'a -> 'a }
 
 let yell s = anomaly s
 
@@ -50,8 +49,7 @@ let default_object s = {
     yell ("The object "^s^" does not know how to substitute!"));
   classify_function = (fun obj -> Keep obj);
   discharge_function = (fun _ -> None);
-  rebuild_function = (fun x -> x);
-  export_function = (fun _ -> None)}
+  rebuild_function = (fun x -> x)}
 
 
 (* The suggested object declaration is the following:
@@ -76,8 +74,7 @@ type dynamic_object_declaration = {
   dyn_subst_function : object_name * substitution * obj -> obj;
   dyn_classify_function : obj -> obj substitutivity;
   dyn_discharge_function : object_name * obj -> obj option;
-  dyn_rebuild_function : obj -> obj;
-  dyn_export_function : obj -> obj option }
+  dyn_rebuild_function : obj -> obj }
 
 let object_tag lobj = Dyn.tag lobj
 
@@ -117,12 +114,6 @@ let declare_object odecl =
   and rebuild lobj =
     if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
     else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
-  and exporter lobj =
-    if Dyn.tag lobj = na then
-      Option.map infun (odecl.export_function (outfun lobj))
-    else
-      anomaly "somehow we got the wrong dynamic object in the exportfun"
-
   in
   Hashtbl.add cache_tab na { dyn_cache_function = cacher;
 			     dyn_load_function = loader;
@@ -130,8 +121,7 @@ let declare_object odecl =
 			     dyn_subst_function = substituter;
 			     dyn_classify_function = classifier;
 			     dyn_discharge_function = discharge;
-			     dyn_rebuild_function = rebuild;
-                             dyn_export_function = exporter };
+			     dyn_rebuild_function = rebuild };
   (infun,outfun)
 
 (* this function describes how the cache, load, open, and export functions
@@ -175,6 +165,3 @@ let discharge_object ((_,lobj) as node) =
 
 let rebuild_object lobj =
   apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
-
-let export_object lobj =
-  apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 6211ab378..834a70c64 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -59,13 +59,6 @@ open Mod_subst
      rebuild the non volatile content of a section from the data
      collected by the discharge function
 
-   * an export function, to enable optional writing of its contents
-     to disk (.vo). This function is also the opportunity to remove
-     redundant information in order to keep .vo size small
-
-     The export function is a little obsolete and will be removed
-     in the near future...
-
 *)
 
 type 'a substitutivity =
@@ -79,8 +72,7 @@ type 'a object_declaration = {
   classify_function : 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
-  rebuild_function : 'a -> 'a;
-  export_function : 'a -> 'a option }
+  rebuild_function : 'a -> 'a }
 
 (* The default object is a "Keep" object with empty methods.
    Object creators are advised to use the construction
@@ -112,7 +104,6 @@ val load_object : int -> object_name * obj -> unit
 val open_object : int -> object_name * obj -> unit
 val subst_object : object_name * substitution * obj -> obj
 val classify_object : obj -> obj substitutivity
-val export_object : obj -> obj option
 val discharge_object : object_name * obj -> obj option
 val rebuild_object : obj -> obj
 val relax : bool -> unit
diff --git a/library/library.ml b/library/library.ml
index 9604a990c..d129a24db 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -304,12 +304,9 @@ let cache_import obj =
 
 let subst_import (_,_,o) = o
 
-let export_import o = Some o
-
 let classify_import (_,export as obj) =
   if export then Substitute obj else Dispose
 
-
 let (in_import, out_import) =
   declare_object {(default_object "IMPORT LIBRARY") with
        cache_function = cache_import;
@@ -523,10 +520,6 @@ let cache_require o =
   load_require 1 o;
   open_require 1 o
 
-  (* keeps the require marker for closed section replay but removes
-     OS dependent fields from .vo files for cross-platform compatibility *)
-let export_require (_,l,e) = Some ([],l,e)
-
 let discharge_require (_,o) = Some o
 
 (* open_function is never called from here because an Anticipate object *)
@@ -536,7 +529,6 @@ let (in_require, out_require) =
        cache_function = cache_require;
        load_function = load_require;
        open_function = (fun _ _ -> assert false);
-       export_function = export_require;
        discharge_function = discharge_require;
        classify_function = (fun o -> Anticipate o) }