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
---
 interp/notation.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 8dec15b602..342cb6c9cf 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -116,15 +116,12 @@ open Libobject
 let classify_scope (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let export_scope (local,_,_ as x) = if local then None else Some x
-
 let (inScope,outScope) =
   declare_object {(default_object "SCOPE") with
       cache_function = cache_scope;
       open_function = open_scope;
       subst_function = subst_scope;
-      classify_function = classify_scope;
-      export_function = export_scope }
+      classify_function = classify_scope }
 
 let open_close_scope (local,opening,sc) =
   Lib.add_anonymous_leaf (inScope (local,opening,Scope sc))
@@ -487,8 +484,7 @@ let (inArgumentsScope,outArgumentsScope) =
       subst_function = subst_arguments_scope;
       classify_function = (fun o -> Substitute o);
       discharge_function = discharge_arguments_scope;
-      rebuild_function = rebuild_arguments_scope;
-      export_function = (fun x -> Some x) }
+      rebuild_function = rebuild_arguments_scope }
 
 let declare_arguments_scope_gen req r scl =
   Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl))
-- 
cgit v1.2.3