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/extraction/table.ml | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 7a265b526f..9451188aaf 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -415,8 +415,7 @@ let (extr_lang,_) =
   declare_object
     {(default_object "Extraction Lang") with
        cache_function = (fun (_,l) -> lang_ref := l);
-       load_function = (fun _ (_,l) -> lang_ref := l);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,l) -> lang_ref := l)}
 
 let _ = declare_summary "Extraction Lang"
 	  { freeze_function = (fun () -> !lang_ref);
@@ -449,7 +448,6 @@ let (inline_extraction,_) =
     {(default_object "Extraction Inline") with
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
-       export_function = (fun x -> Some x);
        classify_function = (fun o -> Substitute o);
        subst_function =
         (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
@@ -492,8 +490,7 @@ let (reset_inline,_) =
   declare_object
     {(default_object "Reset Extraction Inline") with
        cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
-       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table)}
 
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
@@ -530,7 +527,6 @@ let (blacklist_extraction,_) =
     {(default_object "Extraction Blacklist") with
        cache_function = (fun (_,l) -> add_blacklist_entries l);
        load_function = (fun _ (_,l) -> add_blacklist_entries l);
-       export_function = (fun x -> Some x);
        classify_function = (fun o -> Libobject.Keep o);
        subst_function = (fun (_,_,x) -> x)
     }
@@ -558,8 +554,7 @@ let (reset_blacklist,_) =
   declare_object
     {(default_object "Reset Extraction Blacklist") with
        cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
-       load_function = (fun _ (_,_)-> blacklist_table := Idset.empty);
-       export_function = (fun x -> Some x)}
+       load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)}
 
 let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 
@@ -588,7 +583,6 @@ let (in_customs,_) =
     {(default_object "ML extractions") with
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
        load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
-       export_function = (fun x -> Some x);
        classify_function = (fun o -> Substitute o);
        subst_function =
         (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
-- 
cgit v1.2.3