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/funind/indfun_common.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 06f3291fe6..600a9123b4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -352,8 +352,6 @@ let subst_Function (_,subst,finfos) =
 
 let classify_Function infos = Libobject.Substitute infos
 
-let export_Function infos = Some infos
-
 
 let discharge_Function (_,finfos) =
   let function_constant' = Lib.discharge_con finfos.function_constant
@@ -410,7 +408,6 @@ let in_Function,out_Function =
        Libobject.load_function  = load_Function;
        Libobject.classify_function  = classify_Function;
        Libobject.subst_function = subst_Function;
-       Libobject.export_function = export_Function;
        Libobject.discharge_function = discharge_Function
 (*        Libobject.open_function = open_Function; *)
     }
-- 
cgit v1.2.3