Remove useless Liboject.export_function field

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

1 files changed, 2 insertions, 5 deletions

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)