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/typeclasses.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'pretyping/typeclasses.ml')

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