Remove useless Liboject.export_function field

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

3 files changed, 5 insertions, 11 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index a4b4260ad8..35ffda0a1b 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 048ec92de3..057b263948 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 097cba5909..9d35225737 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);