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 ++------ interp/syntax_def.ml | 6 +----- library/declare.ml | 10 ++-------- library/declaremods.ml | 16 +++++----------- library/goptions.ml | 8 ++------ library/heads.ml | 5 +---- library/impargs.ml | 6 +----- library/libobject.ml | 21 ++++----------------- library/libobject.mli | 11 +---------- library/library.ml | 8 -------- plugins/dp/dp.ml | 18 ++++++------------ plugins/extraction/table.ml | 12 +++--------- plugins/field/field.ml4 | 4 +--- plugins/funind/indfun_common.ml | 3 --- plugins/ring/ring.ml | 8 +++----- plugins/setoid_ring/newring.ml4 | 16 ++++++---------- plugins/subtac/subtac_obligations.ml | 3 +-- pretyping/classops.ml | 3 +-- pretyping/recordops.ml | 7 ++----- pretyping/typeclasses.ml | 6 ++---- proofs/redexpr.ml | 9 +-------- tactics/auto.ml | 3 +-- tactics/autorewrite.ml | 5 +---- tactics/dhyp.ml | 3 +-- tactics/extratactics.ml4 | 3 +-- tactics/tacinterp.ml | 3 +-- toplevel/command.ml | 12 ++++-------- toplevel/ind_tables.ml | 12 ------------ toplevel/ind_tables.mli | 5 ----- toplevel/libtypes.ml | 1 - toplevel/metasyntax.ml | 15 +++++---------- toplevel/mltop.ml4 | 3 --- 32 files changed, 59 insertions(+), 194 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index 8dec15b60..342cb6c9c 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)) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index e58bb000a..939fe01aa 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 diff --git a/library/declare.ml b/library/declare.ml index 49b7d7ba2..da723aa4b 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -138,8 +138,6 @@ let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false)) let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk -let export_constant cst = Some (dummy_constant cst) - let classify_constant cst = Substitute (dummy_constant cst) let (inConstant,_) = @@ -149,8 +147,7 @@ let (inConstant,_) = open_function = open_constant; classify_function = classify_constant; subst_function = ident_subst_function; - discharge_function = discharge_constant; - export_function = export_constant } + discharge_function = discharge_constant } let hcons_constant_declaration = function | DefinitionEntry ce when !Flags.hash_cons_proofs -> @@ -259,8 +256,6 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = true; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }) -let export_inductive x = Some (dummy_inductive_entry x) - let (inInductive,_) = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; @@ -268,8 +263,7 @@ let (inInductive,_) = open_function = open_inductive; classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; - discharge_function = discharge_inductive; - export_function = export_inductive } + discharge_function = discharge_inductive } (* for initial declaration *) let declare_mind isrecord mie = diff --git a/library/declaremods.ml b/library/declaremods.ml index 37ee34d1f..d796a2906 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -296,8 +296,7 @@ let (in_module,out_module) = load_function = load_module; open_function = open_module; subst_function = subst_module; - classify_function = classify_module; - export_function = (fun _ -> anomaly "No modules in sections!") } + classify_function = classify_module } let rec replace_alias modalias_obj obj = @@ -456,9 +455,7 @@ let (in_module_alias,out_module_alias) = open_function = open_module_alias; classify_function = classify_module_alias; subst_function = subst_module_alias; - load_function = load_module_alias; - export_function = (fun _ -> anomaly "No modules in sections!") } - + load_function = load_module_alias } @@ -487,8 +484,7 @@ let (in_modkeep,_) = declare_object {(default_object "MODULE KEEP OBJECTS") with cache_function = cache_keep; load_function = load_keep; - open_function = open_keep; - export_function = (fun _ -> anomaly "No modules in sections!") } + open_function = open_keep } (* we remember objects for a module type. In case of a declaration: Module M:SIG:=... @@ -572,8 +568,7 @@ let (in_modtype,_) = open_function = open_modtype; load_function = load_modtype; subst_function = subst_modtype; - classify_function = classify_modtype; - export_function = Option.make } + classify_function = classify_modtype } @@ -1043,8 +1038,7 @@ let (in_include,out_include) = load_function = load_include; open_function = open_include; subst_function = subst_include; - classify_function = classify_include; - export_function = (fun _ -> anomaly "No modules in section!") } + classify_function = classify_include } let rec update_include (sub,mbids,msid,objs) = let rec replace_include = function 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; diff --git a/library/heads.ml b/library/heads.ml index bca6b6502..150ba8942 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -155,8 +155,6 @@ let discharge_head (_,(ref,k)) = let rebuild_head (ref,k) = (ref, compute_head ref) -let export_head o = Some o - let (inHead, _) = declare_object {(default_object "HEAD") with cache_function = cache_head; @@ -164,8 +162,7 @@ let (inHead, _) = subst_function = subst_head; classify_function = (fun x -> Substitute x); discharge_function = discharge_head; - rebuild_function = rebuild_head; - export_function = export_head } + rebuild_function = rebuild_head } let declare_head c = let hd = compute_head c in diff --git a/library/impargs.ml b/library/impargs.ml index edd0aba0e..d27ced220 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -521,9 +521,6 @@ let rebuild_implicits (req,l) = let l' = merge_impls auto m in [ref,l'] in (req,l') -let export_implicits (req,_ as x) = - if req = ImplLocal then None else Some x - let (inImplicits, _) = declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; @@ -531,8 +528,7 @@ let (inImplicits, _) = subst_function = subst_implicits; classify_function = (fun x -> Substitute x); discharge_function = discharge_implicits; - rebuild_function = rebuild_implicits; - export_function = export_implicits } + rebuild_function = rebuild_implicits } let declare_implicits_gen req flags ref = let imps = compute_global_implicits flags [] ref in diff --git a/library/libobject.ml b/library/libobject.ml index 95894294b..9beb32cfc 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -36,8 +36,7 @@ type 'a object_declaration = { classify_function : 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; - rebuild_function : 'a -> 'a; - export_function : 'a -> 'a option } + rebuild_function : 'a -> 'a } let yell s = anomaly s @@ -50,8 +49,7 @@ let default_object s = { yell ("The object "^s^" does not know how to substitute!")); classify_function = (fun obj -> Keep obj); discharge_function = (fun _ -> None); - rebuild_function = (fun x -> x); - export_function = (fun _ -> None)} + rebuild_function = (fun x -> x)} (* The suggested object declaration is the following: @@ -76,8 +74,7 @@ type dynamic_object_declaration = { dyn_subst_function : object_name * substitution * obj -> obj; dyn_classify_function : obj -> obj substitutivity; dyn_discharge_function : object_name * obj -> obj option; - dyn_rebuild_function : obj -> obj; - dyn_export_function : obj -> obj option } + dyn_rebuild_function : obj -> obj } let object_tag lobj = Dyn.tag lobj @@ -117,12 +114,6 @@ let declare_object odecl = and rebuild lobj = if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the rebuildfun" - and exporter lobj = - if Dyn.tag lobj = na then - Option.map infun (odecl.export_function (outfun lobj)) - else - anomaly "somehow we got the wrong dynamic object in the exportfun" - in Hashtbl.add cache_tab na { dyn_cache_function = cacher; dyn_load_function = loader; @@ -130,8 +121,7 @@ let declare_object odecl = dyn_subst_function = substituter; dyn_classify_function = classifier; dyn_discharge_function = discharge; - dyn_rebuild_function = rebuild; - dyn_export_function = exporter }; + dyn_rebuild_function = rebuild }; (infun,outfun) (* this function describes how the cache, load, open, and export functions @@ -175,6 +165,3 @@ let discharge_object ((_,lobj) as node) = let rebuild_object lobj = apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj - -let export_object lobj = - apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj diff --git a/library/libobject.mli b/library/libobject.mli index 6211ab378..834a70c64 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -59,13 +59,6 @@ open Mod_subst rebuild the non volatile content of a section from the data collected by the discharge function - * an export function, to enable optional writing of its contents - to disk (.vo). This function is also the opportunity to remove - redundant information in order to keep .vo size small - - The export function is a little obsolete and will be removed - in the near future... - *) type 'a substitutivity = @@ -79,8 +72,7 @@ type 'a object_declaration = { classify_function : 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; - rebuild_function : 'a -> 'a; - export_function : 'a -> 'a option } + rebuild_function : 'a -> 'a } (* The default object is a "Keep" object with empty methods. Object creators are advised to use the construction @@ -112,7 +104,6 @@ val load_object : int -> object_name * obj -> unit val open_object : int -> object_name * obj -> unit val subst_object : object_name * substitution * obj -> obj val classify_object : obj -> obj substitutivity -val export_object : obj -> obj option val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj val relax : bool -> unit diff --git a/library/library.ml b/library/library.ml index 9604a990c..d129a24db 100644 --- a/library/library.ml +++ b/library/library.ml @@ -304,12 +304,9 @@ let cache_import obj = let subst_import (_,_,o) = o -let export_import o = Some o - let classify_import (_,export as obj) = if export then Substitute obj else Dispose - let (in_import, out_import) = declare_object {(default_object "IMPORT LIBRARY") with cache_function = cache_import; @@ -523,10 +520,6 @@ let cache_require o = load_require 1 o; open_require 1 o - (* keeps the require marker for closed section replay but removes - OS dependent fields from .vo files for cross-platform compatibility *) -let export_require (_,l,e) = Some ([],l,e) - let discharge_require (_,o) = Some o (* open_function is never called from here because an Anticipate object *) @@ -536,7 +529,6 @@ let (in_require, out_require) = cache_function = cache_require; load_function = load_require; open_function = (fun _ _ -> assert false); - export_function = export_require; discharge_function = discharge_require; classify_function = (fun o -> Anticipate o) } diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index dc4698c5e..636504361 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -40,8 +40,7 @@ let (dp_timeout_obj,_) = declare_object {(default_object "Dp_timeout") with cache_function = (fun (_,x) -> set_timeout x); - load_function = (fun _ (_,x) -> set_timeout x); - export_function = (fun x -> Some x)} + load_function = (fun _ (_,x) -> set_timeout x)} let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x) @@ -49,8 +48,7 @@ let (dp_debug_obj,_) = declare_object {(default_object "Dp_debug") with cache_function = (fun (_,x) -> set_debug x); - load_function = (fun _ (_,x) -> set_debug x); - export_function = (fun x -> Some x)} + load_function = (fun _ (_,x) -> set_debug x)} let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x) @@ -58,8 +56,7 @@ let (dp_trace_obj,_) = declare_object {(default_object "Dp_trace") with cache_function = (fun (_,x) -> set_trace x); - load_function = (fun _ (_,x) -> set_trace x); - export_function = (fun x -> Some x)} + load_function = (fun _ (_,x) -> set_trace x)} let dp_trace x = Lib.add_anonymous_leaf (dp_trace_obj x) @@ -818,8 +815,7 @@ let (dp_prelude_obj,_) = declare_object {(default_object "Dp_prelude") with cache_function = (fun (_,x) -> set_prelude x); - load_function = (fun _ (_,x) -> set_prelude x); - export_function = (fun x -> Some x)} + load_function = (fun _ (_,x) -> set_prelude x)} let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x) @@ -1061,8 +1057,7 @@ let (dp_hint_obj,_) = declare_object {(default_object "Dp_hint") with cache_function = (fun (_,l) -> dp_hint l); - load_function = (fun _ (_,l) -> dp_hint l); - export_function = (fun x -> Some x)} + load_function = (fun _ (_,l) -> dp_hint l)} let dp_hint l = Lib.add_anonymous_leaf (dp_hint_obj l) @@ -1088,8 +1083,7 @@ let (dp_predefined_obj,_) = declare_object {(default_object "Dp_predefined") with cache_function = (fun (_,(id,s)) -> dp_predefined id s); - load_function = (fun _ (_,(id,s)) -> dp_predefined id s); - export_function = (fun x -> Some x)} + load_function = (fun _ (_,(id,s)) -> dp_predefined id s)} let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s)) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 7a265b526..9451188aa 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -415,8 +415,7 @@ let (extr_lang,_) = declare_object {(default_object "Extraction Lang") with cache_function = (fun (_,l) -> lang_ref := l); - load_function = (fun _ (_,l) -> lang_ref := l); - export_function = (fun x -> Some x)} + load_function = (fun _ (_,l) -> lang_ref := l)} let _ = declare_summary "Extraction Lang" { freeze_function = (fun () -> !lang_ref); @@ -449,7 +448,6 @@ let (inline_extraction,_) = {(default_object "Extraction Inline") with cache_function = (fun (_,(b,l)) -> add_inline_entries b l); load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); - export_function = (fun x -> Some x); classify_function = (fun o -> Substitute o); subst_function = (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) @@ -492,8 +490,7 @@ let (reset_inline,_) = declare_object {(default_object "Reset Extraction Inline") with cache_function = (fun (_,_)-> inline_table := empty_inline_table); - load_function = (fun _ (_,_)-> inline_table := empty_inline_table); - export_function = (fun x -> Some x)} + load_function = (fun _ (_,_)-> inline_table := empty_inline_table)} let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) @@ -530,7 +527,6 @@ let (blacklist_extraction,_) = {(default_object "Extraction Blacklist") with cache_function = (fun (_,l) -> add_blacklist_entries l); load_function = (fun _ (_,l) -> add_blacklist_entries l); - export_function = (fun x -> Some x); classify_function = (fun o -> Libobject.Keep o); subst_function = (fun (_,_,x) -> x) } @@ -558,8 +554,7 @@ let (reset_blacklist,_) = declare_object {(default_object "Reset Extraction Blacklist") with cache_function = (fun (_,_)-> blacklist_table := Idset.empty); - load_function = (fun _ (_,_)-> blacklist_table := Idset.empty); - export_function = (fun x -> Some x)} + load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)} let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ()) @@ -588,7 +583,6 @@ let (in_customs,_) = {(default_object "ML extractions") with cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s); - export_function = (fun x -> Some x); classify_function = (fun o -> Substitute o); subst_function = (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 2b4651dfb..7ac5f4e89 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -65,7 +65,6 @@ let subst_addfield (_,subst,(typ,th as obj)) = let th' = subst_mps subst th in if typ' == typ && th' == th then obj else (typ',th') -let export_addfield x = Some x (* Declaration of the Add Field library object *) let (in_addfield,out_addfield)= @@ -73,8 +72,7 @@ let (in_addfield,out_addfield)= Libobject.open_function = (fun i o -> if i=1 then cache_addfield o); Libobject.cache_function = cache_addfield; Libobject.subst_function = subst_addfield; - Libobject.classify_function = (fun a -> Libobject.Substitute a); - Libobject.export_function = export_addfield } + Libobject.classify_function = (fun a -> Libobject.Substitute a)} (* Adds a theory to the table *) let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 06f3291fe..600a9123b 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -352,8 +352,6 @@ let subst_Function (_,subst,finfos) = let classify_Function infos = Libobject.Substitute infos -let export_Function infos = Some infos - let discharge_Function (_,finfos) = let function_constant' = Lib.discharge_con finfos.function_constant @@ -410,7 +408,6 @@ let in_Function,out_Function = Libobject.load_function = load_Function; Libobject.classify_function = classify_Function; Libobject.subst_function = subst_Function; - Libobject.export_function = export_Function; Libobject.discharge_function = discharge_Function (* Libobject.open_function = open_Function; *) } diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index bf3b8ef6f..6ee12ebcb 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 *) diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index c6d9bf44a..a930fee17 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 diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 94bd059c2..76a8a0322 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -170,8 +170,7 @@ let (input,output) = prlist_with_sep spc (fun x -> Nameops.pr_id x) (map_keys infos)); Substitute (ProgMap.empty, tac)); - subst_function = subst; - export_function = (fun x -> Some x) } + subst_function = subst} let update_state () = (* msgnl (str "Updating obligations info"); *) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index a4b4260ad..35ffda0a1 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -383,8 +383,7 @@ let (inCoercion,_) = cache_function = cache_coercion; subst_function = subst_coercion; classify_function = (fun x -> Substitute x); - discharge_function = discharge_coercion; - export_function = (function x -> Some x) } + discharge_function = discharge_coercion } let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps = Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps)) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 048ec92de..057b26394 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -78,8 +78,7 @@ let (inStruc,outStruc) = load_function = load_structure; subst_function = subst_structure; classify_function = (fun x -> Substitute x); - discharge_function = discharge_structure; - export_function = (function x -> Some x) } + discharge_function = discharge_structure } let declare_structure (s,c,kl,pl) = Lib.add_anonymous_leaf (inStruc (s,c,kl,pl)) @@ -138,7 +137,6 @@ let (in_method,out_method) = load_function = (fun _ -> load_method); cache_function = load_method; subst_function = (fun (_,s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id); - export_function = (fun x -> Some x); classify_function = (fun x -> Substitute x) } @@ -270,8 +268,7 @@ let (inCanonStruc,outCanonStruct) = cache_function = cache_canonical_structure; subst_function = subst_canonical_structure; classify_function = (fun x -> Substitute x); - discharge_function = discharge_canonical_structure; - export_function = (function x -> Some x) } + discharge_function = discharge_canonical_structure } let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 097cba590..9d3522573 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -169,8 +169,7 @@ let (class_input,class_output) = classify_function = (fun x -> Substitute x); discharge_function = (fun a -> Some (discharge_class a)); rebuild_function = rebuild_class; - subst_function = subst_class; - export_function = (fun x -> Some x) } + subst_function = subst_class } let add_class cl = Lib.add_anonymous_leaf (class_input cl) @@ -213,8 +212,7 @@ let (instance_input,instance_output) = classify_function = (fun x -> Substitute x); discharge_function = (fun a -> Some (discharge_instance a)); rebuild_function = rebuild_instance; - subst_function = subst_instance; - export_function = (fun x -> Some x) } + subst_function = subst_instance } let add_instance i = Lib.add_anonymous_leaf (instance_input i); diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 880efc2d0..d12b5f8e5 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -71,12 +71,6 @@ let map_strategy f l = if ql'=[] then str else (lev,ql')::str) l [] in if l'=[] then None else Some (false,l') -let export_strategy (local,obj) = - if local then None else - map_strategy (function - EvalVarRef _ -> None - | EvalConstRef _ as q -> Some q) obj - let classify_strategy (local,_ as obj) = if local then Dispose else Substitute obj @@ -97,8 +91,7 @@ let (inStrategy,outStrategy) = load_function = (fun _ (_,obj) -> cache_strategy obj); subst_function = subst_strategy; discharge_function = discharge_strategy; - classify_function = classify_strategy; - export_function = export_strategy } + classify_function = classify_strategy } let set_strategy local str = diff --git a/tactics/auto.ml b/tactics/auto.ml index 8b68fa09b..e70279a8d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -457,8 +457,7 @@ let (inAutoHint,_) = cache_function = cache_autohint; load_function = (fun _ -> cache_autohint); subst_function = subst_autohint; - classify_function = classify_autohint; - export_function = export_autohint } + classify_function = classify_autohint } let create_hint_db l n st b = diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index dbaedeefc..6abe8938c 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -215,8 +215,6 @@ let cache_hintrewrite (_,(rbase,lrl)) = let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab -let export_hintrewrite x = Some x - let subst_hintrewrite (_,subst,(rbase,list as node)) = let list' = HintDN.subst subst list in if list' == list then node else @@ -231,8 +229,7 @@ let (inHintRewrite,_)= Libobject.cache_function = cache_hintrewrite; Libobject.load_function = (fun _ -> cache_hintrewrite); Libobject.subst_function = subst_hintrewrite; - Libobject.classify_function = classify_hintrewrite; - Libobject.export_function = export_hintrewrite } + Libobject.classify_function = classify_hintrewrite } open Clenv diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index e3dddacb0..0d4684e22 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -220,8 +220,7 @@ let (inDD,_) = cache_function = cache_dd; open_function = (fun i o -> if i=1 then cache_dd o); subst_function = subst_dd; - classify_function = classify_dd; - export_function = export_dd } + classify_function = classify_dd } let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT")) let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE")) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index c7c235cc0..6ac35317c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -408,8 +408,7 @@ let (inTransitivity,_) = cache_function = cache_transitivity_lemma; open_function = (fun i o -> if i=1 then cache_transitivity_lemma o); subst_function = subst_transitivity_lemma; - classify_function = (fun o -> Substitute o); - export_function = (fun x -> Some x) } + classify_function = (fun o -> Substitute o) } (* Synchronisation with reset *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8e55d4f5c..8d8b94c6c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2836,8 +2836,7 @@ let (inMD,outMD) = load_function = load_md; open_function = open_md; subst_function = subst_md; - classify_function = (fun o -> Substitute o); - export_function = (fun x -> Some x)} + classify_function = (fun o -> Substitute o)} let print_ltac id = try diff --git a/toplevel/command.ml b/toplevel/command.ml index 735e1ff27..3b25f2fa6 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -282,8 +282,7 @@ let (inScheme,_) = declare_object {(default_object "EQSCHEME") with cache_function = Ind_tables.cache_scheme; load_function = (fun _ -> Ind_tables.cache_scheme); - subst_function = Auto_ind_decl.subst_in_constr; - export_function = Ind_tables.export_scheme } + subst_function = Auto_ind_decl.subst_in_constr } let declare_eq_scheme sp = let mib = Global.lookup_mind sp in @@ -315,22 +314,19 @@ let (inBoolLeib,_) = declare_object {(default_object "BOOLLIEB") with cache_function = Ind_tables.cache_bl; load_function = (fun _ -> Ind_tables.cache_bl); - subst_function = Auto_ind_decl.subst_in_constr; - export_function = Ind_tables.export_bool_leib } + subst_function = Auto_ind_decl.subst_in_constr } let (inLeibBool,_) = declare_object {(default_object "LIEBBOOL") with cache_function = Ind_tables.cache_lb; load_function = (fun _ -> Ind_tables.cache_lb); - subst_function = Auto_ind_decl.subst_in_constr; - export_function = Ind_tables.export_leib_bool } + subst_function = Auto_ind_decl.subst_in_constr } let (inDec,_) = declare_object {(default_object "EQDEC") with cache_function = Ind_tables.cache_dec; load_function = (fun _ -> Ind_tables.cache_dec); - subst_function = Auto_ind_decl.subst_in_constr; - export_function = Ind_tables.export_dec_proof } + subst_function = Auto_ind_decl.subst_in_constr } let start_hook = ref ignore let set_start_hook = (:=) start_hook diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 49c8ce715..245f96227 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -16,9 +16,6 @@ let eq_scheme_map = ref Indmap.empty let cache_scheme (_,(ind,const)) = eq_scheme_map := Indmap.add ind const (!eq_scheme_map) -let export_scheme obj = - Some obj - let _ = Summary.declare_summary "eqscheme" @@ -46,15 +43,6 @@ let cache_lb (_,(ind,const)) = let cache_dec (_,(ind,const)) = dec_map := Indmap.add ind const (!dec_map) -let export_bool_leib obj = - Some obj - -let export_leib_bool obj = - Some obj - -let export_dec_proof obj = - Some obj - let _ = Summary.declare_summary "bl_proof" diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index a97c2daaa..e13eedbdc 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -14,7 +14,6 @@ open Sign val cache_scheme :(object_name*(Indmap.key*constr)) -> unit -val export_scheme : (Indmap.key*constr) -> (Indmap.key*constr) option val find_eq_scheme : Indmap.key -> constr val check_eq_scheme : Indmap.key -> bool @@ -23,10 +22,6 @@ val cache_bl: (object_name*(Indmap.key*constr)) -> unit val cache_lb: (object_name*(Indmap.key*constr)) -> unit val cache_dec : (object_name*(Indmap.key*constr)) -> unit -val export_bool_leib : (Indmap.key*constr) -> (Indmap.key*constr) option -val export_leib_bool : (Indmap.key*constr) -> (Indmap.key*constr) option -val export_dec_proof : (Indmap.key*constr) -> (Indmap.key*constr) option - val find_bl_proof : Indmap.key -> constr val find_lb_proof : Indmap.key -> constr val find_eq_dec_proof : Indmap.key -> constr diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index fa636989a..e04480700 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -71,7 +71,6 @@ let (input,output) = { (default_object "LIBTYPES") with load_function = (fun _ -> load); subst_function = (fun (_,s,t) -> subst s t); - export_function = (fun x -> Some x); classify_function = (fun x -> Substitute x) } diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 288f1850e..3595d2dfc 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -35,8 +35,7 @@ let (inToken, outToken) = open_function = (fun i o -> if i=1 then cache_token o); cache_function = cache_token; subst_function = Libobject.ident_subst_function; - classify_function = (fun o -> Substitute o); - export_function = (fun x -> Some x)} + classify_function = (fun o -> Substitute o)} let add_token_obj s = Lib.add_anonymous_leaf (inToken s) @@ -74,8 +73,7 @@ let (inTacticGrammar, outTacticGrammar) = open_function = (fun i o -> if i=1 then cache_tactic_notation o); cache_function = cache_tactic_notation; subst_function = subst_tactic_notation; - classify_function = (fun o -> Substitute o); - export_function = (fun x -> Some x)} + classify_function = (fun o -> Substitute o)} let cons_production_parameter l = function | GramTerminal _ -> l @@ -693,8 +691,7 @@ let (inSyntaxExtension, outSyntaxExtension) = open_function = (fun i o -> if i=1 then cache_syntax_extension o); cache_function = cache_syntax_extension; subst_function = subst_syntax_extension; - classify_function = classify_syntax_definition; - export_function = export_syntax_definition} + classify_function = classify_syntax_definition} (**************************************************************************) (* Precedences *) @@ -886,8 +883,7 @@ let (inNotation, outNotation) = cache_function = cache_notation; subst_function = subst_notation; load_function = load_notation; - classify_function = classify_notation; - export_function = export_notation} + classify_function = classify_notation} (**********************************************************************) (* Recovering existing syntax *) @@ -1046,8 +1042,7 @@ let (inScopeCommand,outScopeCommand) = open_function = open_scope_command; load_function = load_scope_command; subst_function = subst_scope_command; - classify_function = (fun obj -> Substitute obj); - export_function = (fun x -> Some x) } + classify_function = (fun obj -> Substitute obj)} let add_delimiters scope key = Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key)) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index e33363f3a..eb9359107 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -299,13 +299,10 @@ let cache_ml_module_object (_,{mnames=mnames}) = error ("Dynamic link not supported (module "^name^")"))) mnames -let export_ml_module_object x = Some x - let (inMLModule,outMLModule) = declare_object {(default_object "ML-MODULE") with load_function = (fun _ -> cache_ml_module_object); cache_function = cache_ml_module_object; - export_function = export_ml_module_object; subst_function = (fun (_,_,o) -> o); classify_function = (fun o -> Substitute o) } -- cgit v1.2.3