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/setoid_ring/newring.ml4 | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index c6d9bf44a0..a930fee17b 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -440,16 +440,14 @@ let subst_th (_,subst,th) =
       ring_post_tac = posttac' }
 
 
-let (theory_to_obj, obj_to_theory) = 
-  let cache_th (name,th) = add_entry name th
-  and export_th x = Some x in
+let (theory_to_obj, obj_to_theory) =
+  let cache_th (name,th) = add_entry name th in
   declare_object
     {(default_object "tactic-new-ring-theory") with
       open_function = (fun i o -> if i=1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
-      classify_function = (fun x -> Substitute x);
-      export_function = export_th }
+      classify_function = (fun x -> Substitute x)}
 
 
 let setoid_of_relation env a r =
@@ -1018,16 +1016,14 @@ let subst_th (_,subst,th) =
       field_pre_tac = pretac';
       field_post_tac = posttac' }
 
-let (ftheory_to_obj, obj_to_ftheory) = 
-  let cache_th (name,th) = add_field_entry name th
-  and export_th x = Some x in
+let (ftheory_to_obj, obj_to_ftheory) =
+  let cache_th (name,th) = add_field_entry name th in
   declare_object
     {(default_object "tactic-new-field-theory") with
       open_function = (fun i o -> if i=1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
-      classify_function = (fun x -> Substitute x);
-      export_function = export_th }
+      classify_function = (fun x -> Substitute x) }
 
 let field_equality r inv req =
   match kind_of_term req with
-- 
cgit v1.2.3