From f8a790f577366f74645d15e767ce827dfa1f0908 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 17 Sep 2009 15:58:38 +0000
Subject: Remove useless Liboject.export_function field

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12338 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/recordops.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'pretyping/recordops.ml')

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)
 
-- 
cgit v1.2.3