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
---
 plugins/field/field.ml4 | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'plugins/field')

diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 2b4651dfb9..7ac5f4e89e 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -65,7 +65,6 @@ let subst_addfield (_,subst,(typ,th as obj)) =
   let th' = subst_mps subst th in
     if typ' == typ && th' == th then obj else
       (typ',th')
-let export_addfield x = Some x
 
 (* Declaration of the Add Field library object *)
 let (in_addfield,out_addfield)=
@@ -73,8 +72,7 @@ let (in_addfield,out_addfield)=
        Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
        Libobject.cache_function = cache_addfield;
        Libobject.subst_function = subst_addfield;
-       Libobject.classify_function = (fun a -> Libobject.Substitute a);
-       Libobject.export_function = export_addfield }
+       Libobject.classify_function = (fun a -> Libobject.Substitute a)}
 
 (* Adds a theory to the table *)
 let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
-- 
cgit v1.2.3