Remove useless Liboject.export_function field

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

32 files changed, 59 insertions, 194 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 8dec15b60..342cb6c9c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -116,15 +116,12 @@ open Libobject
 let classify_scope (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let export_scope (local,_,_ as x) = if local then None else Some x
-
 let (inScope,outScope) =
   declare_object {(default_object "SCOPE") with
       cache_function = cache_scope;
       open_function = open_scope;
       subst_function = subst_scope;
-      classify_function = classify_scope;
-      export_function = export_scope }
+      classify_function = classify_scope }
 
 let open_close_scope (local,opening,sc) =
   Lib.add_anonymous_leaf (inScope (local,opening,Scope sc))
@@ -487,8 +484,7 @@ let (inArgumentsScope,outArgumentsScope) =
       subst_function = subst_arguments_scope;
       classify_function = (fun o -> Substitute o);
       discharge_function = discharge_arguments_scope;
-      rebuild_function = rebuild_arguments_scope;
-      export_function = (fun x -> Some x) }
+      rebuild_function = rebuild_arguments_scope }
 
 let declare_arguments_scope_gen req r scl =
   Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl))
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index e58bb000a..939fe01aa 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -57,17 +57,13 @@ let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) =
 let classify_syntax_constant (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let export_syntax_constant (local,_,_ as o) =
-  if local then None else Some o
-
 let (in_syntax_constant, out_syntax_constant) =
   declare_object {(default_object "SYNTAXCONSTANT") with
     cache_function = cache_syntax_constant;
     load_function = load_syntax_constant;
     open_function = open_syntax_constant;
     subst_function = subst_syntax_constant;
-    classify_function = classify_syntax_constant;
-    export_function = export_syntax_constant } 
+    classify_function = classify_syntax_constant }
 
 type syndef_interpretation = (identifier * subscopes) list * aconstr
 
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) }
 
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index dc4698c5e..636504361 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -40,8 +40,7 @@ let (dp_timeout_obj,_) =
   declare_object
     {(default_object "Dp_timeout") with
        cache_function = (fun (_,x) -> set_timeout x);
-       load_function = (fun _ (_,x) -> set_timeout x);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,x) -> set_timeout x)}
 
 let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
 
@@ -49,8 +48,7 @@ let (dp_debug_obj,_) =
   declare_object
     {(default_object "Dp_debug") with
        cache_function = (fun (_,x) -> set_debug x);
-       load_function = (fun _ (_,x) -> set_debug x);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,x) -> set_debug x)}
 
 let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
 
@@ -58,8 +56,7 @@ let (dp_trace_obj,_) =
   declare_object
     {(default_object "Dp_trace") with
        cache_function = (fun (_,x) -> set_trace x);
-       load_function = (fun _ (_,x) -> set_trace x);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,x) -> set_trace x)}
 
 let dp_trace x = Lib.add_anonymous_leaf (dp_trace_obj x)
 
@@ -818,8 +815,7 @@ let (dp_prelude_obj,_) =
   declare_object
     {(default_object "Dp_prelude") with
        cache_function = (fun (_,x) -> set_prelude x);
-       load_function = (fun _ (_,x) -> set_prelude x);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,x) -> set_prelude x)}
 
 let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x)
 
@@ -1061,8 +1057,7 @@ let (dp_hint_obj,_) =
   declare_object
     {(default_object "Dp_hint") with
        cache_function = (fun (_,l) -> dp_hint l);
-       load_function = (fun _ (_,l) -> dp_hint l);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,l) -> dp_hint l)}
 
 let dp_hint l = Lib.add_anonymous_leaf (dp_hint_obj l)
 
@@ -1088,8 +1083,7 @@ let (dp_predefined_obj,_) =
   declare_object
     {(default_object "Dp_predefined") with
        cache_function = (fun (_,(id,s)) -> dp_predefined id s);
-       load_function = (fun _ (_,(id,s)) -> dp_predefined id s);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,(id,s)) -> dp_predefined id s)}
 
 let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s))
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 7a265b526..9451188aa 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -415,8 +415,7 @@ let (extr_lang,_) =
   declare_object
     {(default_object "Extraction Lang") with
        cache_function = (fun (_,l) -> lang_ref := l);
-       load_function = (fun _ (_,l) -> lang_ref := l);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,l) -> lang_ref := l)}
 
 let _ = declare_summary "Extraction Lang"
 	  { freeze_function = (fun () -> !lang_ref);
@@ -449,7 +448,6 @@ let (inline_extraction,_) =
     {(default_object "Extraction Inline") with
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
-       export_function = (fun x -> Some x);
        classify_function = (fun o -> Substitute o);
        subst_function =
         (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
@@ -492,8 +490,7 @@ let (reset_inline,_) =
   declare_object
     {(default_object "Reset Extraction Inline") with
        cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
-       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table)}
 
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
@@ -530,7 +527,6 @@ let (blacklist_extraction,_) =
     {(default_object "Extraction Blacklist") with
        cache_function = (fun (_,l) -> add_blacklist_entries l);
        load_function = (fun _ (_,l) -> add_blacklist_entries l);
-       export_function = (fun x -> Some x);
        classify_function = (fun o -> Libobject.Keep o);
        subst_function = (fun (_,_,x) -> x)
     }
@@ -558,8 +554,7 @@ let (reset_blacklist,_) =
   declare_object
     {(default_object "Reset Extraction Blacklist") with
        cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
-       load_function = (fun _ (_,_)-> blacklist_table := Idset.empty);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)}
 
 let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 
@@ -588,7 +583,6 @@ let (in_customs,_) =
     {(default_object "ML extractions") with
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
        load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
-       export_function = (fun x -> Some x);
        classify_function = (fun o -> Substitute o);
        subst_function =
         (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 2b4651dfb..7ac5f4e89 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -65,7 +65,6 @@ let subst_addfield (_,subst,(typ,th as obj)) =
   let th' = subst_mps subst th in
     if typ' == typ && th' == th then obj else
       (typ',th')
-let export_addfield x = Some x
 
 (* Declaration of the Add Field library object *)
 let (in_addfield,out_addfield)=
@@ -73,8 +72,7 @@ let (in_addfield,out_addfield)=
        Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
        Libobject.cache_function = cache_addfield;
        Libobject.subst_function = subst_addfield;
-       Libobject.classify_function = (fun a -> Libobject.Substitute a);
-       Libobject.export_function = export_addfield }
+       Libobject.classify_function = (fun a -> Libobject.Substitute a)}
 
 (* Adds a theory to the table *)
 let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 06f3291fe..600a9123b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -352,8 +352,6 @@ let subst_Function (_,subst,finfos) =
 
 let classify_Function infos = Libobject.Substitute infos
 
-let export_Function infos = Some infos
-
 
 let discharge_Function (_,finfos) =
   let function_constant' = Lib.discharge_con finfos.function_constant
@@ -410,7 +408,6 @@ let in_Function,out_Function =
        Libobject.load_function  = load_Function;
        Libobject.classify_function  = classify_Function;
        Libobject.subst_function = subst_Function;
-       Libobject.export_function = export_Function;
        Libobject.discharge_function = discharge_Function
 (*        Libobject.open_function = open_Function; *)
     }
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index bf3b8ef6f..6ee12ebcb 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -265,15 +265,13 @@ let subst_th (_,subst,(c,th as obj)) =
       (c',th')
 
 
-let (theory_to_obj, obj_to_theory) = 
-  let cache_th (_,(c, th)) = theories_map_add (c,th)
-  and export_th x = Some x in
+let (theory_to_obj, obj_to_theory) =
+  let cache_th (_,(c, th)) = theories_map_add (c,th) in
   declare_object {(default_object "tactic-ring-theory") with
 		    open_function = (fun i o -> if i=1 then cache_th o);
                     cache_function = cache_th;
 		    subst_function = subst_th;
-		    classify_function = (fun x -> Substitute x);
-		    export_function = export_th }
+		    classify_function = (fun x -> Substitute x) }
 
 (* from the set A, guess the associated theory *)
 (* With this simple solution, the theory to use is automatically guessed *)
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index c6d9bf44a..a930fee17 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -440,16 +440,14 @@ let subst_th (_,subst,th) =
       ring_post_tac = posttac' }
 
 
-let (theory_to_obj, obj_to_theory) = 
-  let cache_th (name,th) = add_entry name th
-  and export_th x = Some x in
+let (theory_to_obj, obj_to_theory) =
+  let cache_th (name,th) = add_entry name th in
   declare_object
     {(default_object "tactic-new-ring-theory") with
       open_function = (fun i o -> if i=1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
-      classify_function = (fun x -> Substitute x);
-      export_function = export_th }
+      classify_function = (fun x -> Substitute x)}
 
 
 let setoid_of_relation env a r =
@@ -1018,16 +1016,14 @@ let subst_th (_,subst,th) =
       field_pre_tac = pretac';
       field_post_tac = posttac' }
 
-let (ftheory_to_obj, obj_to_ftheory) = 
-  let cache_th (name,th) = add_field_entry name th
-  and export_th x = Some x in
+let (ftheory_to_obj, obj_to_ftheory) =
+  let cache_th (name,th) = add_field_entry name th in
   declare_object
     {(default_object "tactic-new-field-theory") with
       open_function = (fun i o -> if i=1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
-      classify_function = (fun x -> Substitute x);
-      export_function = export_th }
+      classify_function = (fun x -> Substitute x) }
 
 let field_equality r inv req =
   match kind_of_term req with
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 94bd059c2..76a8a0322 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -170,8 +170,7 @@ let (input,output) =
 				   prlist_with_sep spc (fun x -> Nameops.pr_id x)
 				   (map_keys infos));
 	Substitute (ProgMap.empty, tac));
-      subst_function = subst;
-      export_function = (fun x -> Some x) }
+      subst_function = subst}
 
 let update_state () =
 (*   msgnl (str "Updating obligations info"); *)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index a4b4260ad..35ffda0a1 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -383,8 +383,7 @@ let (inCoercion,_) =
     cache_function = cache_coercion;
     subst_function = subst_coercion;
     classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_coercion;
-    export_function = (function x -> Some x)  }
+    discharge_function = discharge_coercion }
 
 let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps =
   Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps))
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 048ec92de..057b26394 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -78,8 +78,7 @@ let (inStruc,outStruc) =
     load_function = load_structure;
     subst_function = subst_structure;
     classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_structure;
-    export_function = (function x -> Some x) }
+    discharge_function = discharge_structure }
 
 let declare_structure (s,c,kl,pl) =
   Lib.add_anonymous_leaf (inStruc (s,c,kl,pl))
@@ -138,7 +137,6 @@ let (in_method,out_method) =
 	load_function = (fun _ -> load_method);
 	cache_function = load_method;
 	subst_function = (fun (_,s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id);
-	export_function = (fun x -> Some x);
 	classify_function = (fun x -> Substitute x)
     }
 
@@ -270,8 +268,7 @@ let (inCanonStruc,outCanonStruct) =
     cache_function = cache_canonical_structure;
     subst_function = subst_canonical_structure;
     classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_canonical_structure;
-    export_function = (function x -> Some x) }
+    discharge_function = discharge_canonical_structure }
 
 let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 097cba590..9d3522573 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -169,8 +169,7 @@ let (class_input,class_output) =
       classify_function = (fun x -> Substitute x);
       discharge_function = (fun a -> Some (discharge_class a));
       rebuild_function = rebuild_class;
-      subst_function = subst_class;
-      export_function = (fun x -> Some x) }
+      subst_function = subst_class }
 
 let add_class cl =
   Lib.add_anonymous_leaf (class_input cl)
@@ -213,8 +212,7 @@ let (instance_input,instance_output) =
       classify_function = (fun x -> Substitute x);
       discharge_function = (fun a -> Some (discharge_instance a));
       rebuild_function = rebuild_instance;
-      subst_function = subst_instance;
-      export_function = (fun x -> Some x) }
+      subst_function = subst_instance }
 
 let add_instance i =
   Lib.add_anonymous_leaf (instance_input i);
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 880efc2d0..d12b5f8e5 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -71,12 +71,6 @@ let map_strategy f l =
       if ql'=[] then str else (lev,ql')::str) l [] in
   if l'=[] then None else Some (false,l')
 
-let export_strategy (local,obj) =
-  if local then None else
-  map_strategy (function
-      EvalVarRef _ -> None
-    | EvalConstRef _ as q -> Some q) obj
-
 let classify_strategy (local,_ as obj) =
   if local then Dispose else Substitute obj
 
@@ -97,8 +91,7 @@ let (inStrategy,outStrategy) =
 		    load_function = (fun _ (_,obj) -> cache_strategy obj);
 		    subst_function = subst_strategy;
                     discharge_function = discharge_strategy;
-		    classify_function = classify_strategy;
-                    export_function = export_strategy }
+		    classify_function = classify_strategy }
 
 
 let set_strategy local str =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8b68fa09b..e70279a8d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -457,8 +457,7 @@ let (inAutoHint,_) =
                     cache_function = cache_autohint;
 		    load_function = (fun _ -> cache_autohint);
 		    subst_function = subst_autohint;
-		    classify_function = classify_autohint;
-                    export_function = export_autohint }
+		    classify_function = classify_autohint }
 
 
 let create_hint_db l n st b =
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index dbaedeefc..6abe8938c 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -215,8 +215,6 @@ let cache_hintrewrite (_,(rbase,lrl)) =
   let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
     rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab
 
-let export_hintrewrite x = Some x
-
 let subst_hintrewrite (_,subst,(rbase,list as node)) =
   let list' = HintDN.subst subst list in
     if list' == list then node else
@@ -231,8 +229,7 @@ let (inHintRewrite,_)=
     Libobject.cache_function = cache_hintrewrite;
     Libobject.load_function = (fun _ -> cache_hintrewrite);
     Libobject.subst_function = subst_hintrewrite;
-    Libobject.classify_function = classify_hintrewrite;
-    Libobject.export_function = export_hintrewrite }
+    Libobject.classify_function = classify_hintrewrite }
 
 
 open Clenv
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index e3dddacb0..0d4684e22 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -220,8 +220,7 @@ let (inDD,_) =
                     cache_function = cache_dd;
 		    open_function = (fun i o -> if i=1 then cache_dd o);
                     subst_function = subst_dd;
-		    classify_function = classify_dd;
-                    export_function = export_dd }
+		    classify_function = classify_dd }
 
 let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT"))
 let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE"))
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c7c235cc0..6ac35317c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -408,8 +408,7 @@ let (inTransitivity,_) =
     cache_function = cache_transitivity_lemma;
     open_function = (fun i o -> if i=1 then cache_transitivity_lemma o);
     subst_function = subst_transitivity_lemma;
-    classify_function = (fun o -> Substitute o);
-    export_function = (fun x -> Some x) }
+    classify_function = (fun o -> Substitute o) }
 
 (* Synchronisation with reset *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8e55d4f5c..8d8b94c6c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2836,8 +2836,7 @@ let (inMD,outMD) =
      load_function   = load_md;
      open_function   = open_md;
      subst_function = subst_md;
-     classify_function = (fun o -> Substitute o);
-     export_function = (fun x -> Some x)}
+     classify_function = (fun o -> Substitute o)}
 
 let print_ltac id =
  try
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 735e1ff27..3b25f2fa6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -282,8 +282,7 @@ let (inScheme,_) =
   declare_object {(default_object "EQSCHEME") with
                     cache_function = Ind_tables.cache_scheme;
                     load_function = (fun _ -> Ind_tables.cache_scheme);
-                    subst_function = Auto_ind_decl.subst_in_constr;
-                    export_function = Ind_tables.export_scheme }
+                    subst_function = Auto_ind_decl.subst_in_constr }
 
 let declare_eq_scheme sp =
   let mib = Global.lookup_mind sp in
@@ -315,22 +314,19 @@ let (inBoolLeib,_) =
   declare_object {(default_object "BOOLLIEB") with
                     cache_function = Ind_tables.cache_bl;
                     load_function = (fun _ -> Ind_tables.cache_bl);
-                    subst_function = Auto_ind_decl.subst_in_constr;
-                    export_function = Ind_tables.export_bool_leib }
+                    subst_function = Auto_ind_decl.subst_in_constr }
 
 let (inLeibBool,_) =
   declare_object {(default_object "LIEBBOOL") with
                     cache_function = Ind_tables.cache_lb;
                     load_function = (fun _ -> Ind_tables.cache_lb);
-                    subst_function = Auto_ind_decl.subst_in_constr;
-                    export_function = Ind_tables.export_leib_bool }
+                    subst_function = Auto_ind_decl.subst_in_constr }
 
 let (inDec,_) =
   declare_object {(default_object "EQDEC") with
                     cache_function = Ind_tables.cache_dec;
                     load_function = (fun _ -> Ind_tables.cache_dec);
-                    subst_function = Auto_ind_decl.subst_in_constr;
-                    export_function = Ind_tables.export_dec_proof }
+                    subst_function = Auto_ind_decl.subst_in_constr }
 
 let start_hook = ref ignore
 let set_start_hook = (:=) start_hook
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 49c8ce715..245f96227 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -16,9 +16,6 @@ let eq_scheme_map = ref Indmap.empty
 let cache_scheme (_,(ind,const)) =
     eq_scheme_map := Indmap.add ind const (!eq_scheme_map)
 
-let export_scheme obj =
-    Some obj
-
 
 
 let _ = Summary.declare_summary "eqscheme"
@@ -46,15 +43,6 @@ let cache_lb (_,(ind,const)) =
 let cache_dec (_,(ind,const)) =
     dec_map := Indmap.add ind const (!dec_map)
 
-let export_bool_leib obj =
-    Some obj
-
-let export_leib_bool obj =
-    Some obj
-
-let export_dec_proof obj =
-    Some obj
-
 
 
 let _ = Summary.declare_summary "bl_proof"
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index a97c2daaa..e13eedbdc 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -14,7 +14,6 @@ open Sign
 
 
 val cache_scheme :(object_name*(Indmap.key*constr)) -> unit
-val export_scheme : (Indmap.key*constr) -> (Indmap.key*constr) option 
 
 val find_eq_scheme : Indmap.key -> constr
 val check_eq_scheme : Indmap.key -> bool
@@ -23,10 +22,6 @@ val cache_bl: (object_name*(Indmap.key*constr)) -> unit
 val cache_lb: (object_name*(Indmap.key*constr)) -> unit
 val cache_dec : (object_name*(Indmap.key*constr)) -> unit
 
-val export_bool_leib : (Indmap.key*constr) -> (Indmap.key*constr) option 
-val export_leib_bool : (Indmap.key*constr) -> (Indmap.key*constr) option 
-val export_dec_proof : (Indmap.key*constr) -> (Indmap.key*constr) option 
-
 val find_bl_proof : Indmap.key -> constr
 val find_lb_proof : Indmap.key -> constr
 val find_eq_dec_proof : Indmap.key -> constr
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index fa636989a..e04480700 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.ml
@@ -71,7 +71,6 @@ let (input,output) =
     { (default_object "LIBTYPES") with
 	load_function = (fun _ -> load);
 	subst_function = (fun (_,s,t) -> subst s t);
-	export_function = (fun x -> Some x);
 	classify_function = (fun x -> Substitute x)
     }
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 288f1850e..3595d2dfc 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -35,8 +35,7 @@ let (inToken, outToken) =
        open_function = (fun i o -> if i=1 then cache_token o);
        cache_function = cache_token;
        subst_function = Libobject.ident_subst_function;
-       classify_function = (fun o -> Substitute o);
-       export_function = (fun x -> Some x)}
+       classify_function = (fun o -> Substitute o)}
 
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
@@ -74,8 +73,7 @@ let (inTacticGrammar, outTacticGrammar) =
        open_function = (fun i o -> if i=1 then cache_tactic_notation o);
        cache_function = cache_tactic_notation;
        subst_function = subst_tactic_notation;
-       classify_function = (fun o -> Substitute o);
-       export_function = (fun x -> Some x)}
+       classify_function = (fun o -> Substitute o)}
 
 let cons_production_parameter l = function
   | GramTerminal _ -> l
@@ -693,8 +691,7 @@ let (inSyntaxExtension, outSyntaxExtension) =
        open_function = (fun i o -> if i=1 then cache_syntax_extension o);
        cache_function = cache_syntax_extension;
        subst_function = subst_syntax_extension;
-       classify_function = classify_syntax_definition;
-       export_function = export_syntax_definition}
+       classify_function = classify_syntax_definition}
 
 (**************************************************************************)
 (* Precedences                                                            *)
@@ -886,8 +883,7 @@ let (inNotation, outNotation) =
        cache_function = cache_notation;
        subst_function = subst_notation;
        load_function = load_notation;
-       classify_function = classify_notation;
-       export_function = export_notation}
+       classify_function = classify_notation}
 
 (**********************************************************************)
 (* Recovering existing syntax                                         *)
@@ -1046,8 +1042,7 @@ let (inScopeCommand,outScopeCommand) =
       open_function = open_scope_command;
       load_function = load_scope_command;
       subst_function = subst_scope_command;
-      classify_function = (fun obj -> Substitute obj);
-      export_function = (fun x -> Some x) }
+      classify_function = (fun obj -> Substitute obj)}
 
 let add_delimiters scope key =
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key))
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index e33363f3a..eb9359107 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -299,13 +299,10 @@ let cache_ml_module_object (_,{mnames=mnames}) =
 	      error ("Dynamic link not supported (module "^name^")")))
     mnames
 
-let export_ml_module_object x = Some x
-					 
 let (inMLModule,outMLModule) =
   declare_object {(default_object "ML-MODULE") with
                     load_function = (fun _ -> cache_ml_module_object);
                     cache_function = cache_ml_module_object;
-                    export_function = export_ml_module_object;
                     subst_function = (fun (_,_,o) -> o);
                     classify_function = (fun o -> Substitute o) }