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/ring/ring.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'plugins/ring')

diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index bf3b8ef6f8..6ee12ebcb3 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -265,15 +265,13 @@ let subst_th (_,subst,(c,th as obj)) =
       (c',th')
 
 
-let (theory_to_obj, obj_to_theory) = 
-  let cache_th (_,(c, th)) = theories_map_add (c,th)
-  and export_th x = Some x in
+let (theory_to_obj, obj_to_theory) =
+  let cache_th (_,(c, th)) = theories_map_add (c,th) in
   declare_object {(default_object "tactic-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) }
 
 (* from the set A, guess the associated theory *)
 (* With this simple solution, the theory to use is automatically guessed *)
-- 
cgit v1.2.3