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 --- library/goptions.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'library/goptions.ml') diff --git a/library/goptions.ml b/library/goptions.ml index e4c5a6155..032016c3d 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -96,15 +96,13 @@ module MakeTable = if p' == p then obj else (f,p') in - let export_options fp = Some fp in let (inGo,outGo) = Libobject.declare_object {(Libobject.default_object nick) with Libobject.load_function = load_options; Libobject.open_function = load_options; Libobject.cache_function = cache_options; Libobject.subst_function = subst_options; - Libobject.classify_function = (fun x -> Substitute x); - Libobject.export_function = export_options} + Libobject.classify_function = (fun x -> Substitute x)} in ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) @@ -255,9 +253,7 @@ let declare_option cast uncast cache_function = (fun (_,v) -> write v); classify_function = (fun v -> Keep v); discharge_function = (fun (_,v) -> Some v); - load_function = (fun _ (_,v) -> write v); - (* spiwack: I'm unsure whether this function does anyting *) - export_function = (fun v -> Some v)} + load_function = (fun _ (_,v) -> write v)} in let _ = declare_summary (nickname key) { freeze_function = read; -- cgit v1.2.3