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/classops.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/classops.ml')

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