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/syntax_def.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'interp/syntax_def.ml')

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index e58bb000a0..939fe01aa4 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -57,17 +57,13 @@ let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) =
 let classify_syntax_constant (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let export_syntax_constant (local,_,_ as o) =
-  if local then None else Some o
-
 let (in_syntax_constant, out_syntax_constant) =
   declare_object {(default_object "SYNTAXCONSTANT") with
     cache_function = cache_syntax_constant;
     load_function = load_syntax_constant;
     open_function = open_syntax_constant;
     subst_function = subst_syntax_constant;
-    classify_function = classify_syntax_constant;
-    export_function = export_syntax_constant } 
+    classify_function = classify_syntax_constant }
 
 type syndef_interpretation = (identifier * subscopes) list * aconstr
 
-- 
cgit v1.2.3