Remove useless Liboject.export_function field

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

6 files changed, 9 insertions, 39 deletions

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) }