diff options
38 files changed, 71 insertions, 178 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 2857f9ad8..08936759d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -768,6 +768,4 @@ let _ = declare_summary "symbols" { freeze_function = freeze; unfreeze_function = unfreeze; - init_function = init; - survive_module = false; - survive_section = false } + init_function = init } diff --git a/interp/reserve.ml b/interp/reserve.ml index f49c42a55..93fc60dfb 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -31,9 +31,7 @@ let _ = Summary.declare_summary "reserved-type" { Summary.freeze_function = (fun () -> !reserve_table); Summary.unfreeze_function = (fun r -> reserve_table := r); - Summary.init_function = (fun () -> reserve_table := Idmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = (fun () -> reserve_table := Idmap.empty) } let declare_reserved_type (loc,id) t = if id <> root_of_id id then diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index ef5ecf62a..1619bad27 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -26,9 +26,7 @@ let _ = Summary.declare_summary "SYNTAXCONSTANT" { Summary.freeze_function = (fun () -> !syntax_table); Summary.unfreeze_function = (fun ft -> syntax_table := ft); - Summary.init_function = (fun () -> syntax_table := KNmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = (fun () -> syntax_table := KNmap.empty) } let add_syntax_constant kn c = syntax_table := KNmap.add kn c !syntax_table diff --git a/library/declaremods.ml b/library/declaremods.ml index 0aa3d96bb..581e3fd5b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -100,9 +100,7 @@ let _ = Summary.declare_summary "MODULE-INFO" modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; openmod_info := ([],None,None); - library_cache := Dirmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + library_cache := Dirmap.empty) } (* auxiliary functions to transform full_path and kernel_name given by Lib into module_path and dir_path needed for modules *) @@ -512,9 +510,7 @@ let _ = Summary.declare_summary "MODTYPE-INFO" openmodtype_info := snd ft); Summary.init_function = (fun () -> modtypetab := MPmap.empty; - openmodtype_info := []); - Summary.survive_module = false; - Summary.survive_section = true } + openmodtype_info := []) } let cache_modtype ((sp,kn),(entry,modtypeobjs)) = @@ -754,15 +750,13 @@ let end_module () = dependencies on functor arguments *) let id = basename (fst oldoname) in - let mp = Global.end_module id res_o in + let mp = Global.end_module fs id res_o in begin match sub_o with None -> () | Some sub_mtb -> check_subtypes mp sub_mtb end; - Summary.module_unfreeze_summaries fs; - let substituted = subst_substobjs dir mp substobjs in let node = in_module (None,substobjs,substituted) in let objects = @@ -885,17 +879,15 @@ let end_modtype () = let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in let id = basename (fst oldoname) in - let ln = Global.end_modtype id in let substitute, _, special = Lib.classify_segment lib_stack in let msid = msid_of_prefix prefix in let mbids = !openmodtype_info in - - Summary.module_unfreeze_summaries fs; - let modtypeobjs = empty_subst, mbids, msid, substitute in + let ln = Global.end_modtype fs id in let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in + if fst oname <> fst oldoname then anomaly "Section paths generated on start_ and end_modtype do not match"; @@ -970,8 +962,8 @@ let rec get_module_substobjs env = function (map_mbid mbid mp (Some resolve))) , mbids, msid, objs) | [] -> match mexpr with - | MSEident _ -> error "Application of a non-functor" - | _ -> error "Application of a functor with too few arguments") + | MSEident _ -> error "Application of a non-functor." + | _ -> error "Application of a functor with too few arguments.") | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty diff --git a/library/decls.ml b/library/decls.ml index 5a8729215..d5d0cb096 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -27,9 +27,7 @@ let vartab = ref (Idmap.empty : variable_data Idmap.t) let _ = Summary.declare_summary "VARIABLE" { Summary.freeze_function = (fun () -> !vartab); Summary.unfreeze_function = (fun ft -> vartab := ft); - Summary.init_function = (fun () -> vartab := Idmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = (fun () -> vartab := Idmap.empty) } let add_variable_data id o = vartab := Idmap.add id o !vartab @@ -47,9 +45,7 @@ let csttab = ref (Cmap.empty : logical_kind Cmap.t) let _ = Summary.declare_summary "CONSTANT" { Summary.freeze_function = (fun () -> !csttab); Summary.unfreeze_function = (fun ft -> csttab := ft); - Summary.init_function = (fun () -> csttab := Cmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = (fun () -> csttab := Cmap.empty) } let add_constant_kind kn k = csttab := Cmap.add kn k !csttab diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 7812b1f9e..ed375a831 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -46,6 +46,4 @@ let _ = Summary.declare_summary "discharged_hypothesis" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = true } + Summary.init_function = init } diff --git a/library/global.ml b/library/global.ml index 4f3a40a8a..ec41c0706 100644 --- a/library/global.ml +++ b/library/global.ml @@ -31,9 +31,7 @@ let _ = declare_summary "Global environment" { freeze_function = (fun () -> !global_env); unfreeze_function = (fun fr -> global_env := fr); - init_function = (fun () -> global_env := empty_environment); - survive_module = true; - survive_section = false } + init_function = (fun () -> global_env := empty_environment) } (* Then we export the functions of [Typing] on that environment. *) @@ -82,9 +80,10 @@ let start_module id = global_env := newenv; mp -let end_module id mtyo = +let end_module fs id mtyo = let l = label_of_id id in let mp,newenv = end_module l mtyo !global_env in + Summary.unfreeze_summaries fs; global_env := newenv; mp @@ -100,9 +99,10 @@ let start_modtype id = global_env := newenv; mp -let end_modtype id = +let end_modtype fs id = let l = label_of_id id in let kn,newenv = end_modtype l !global_env in + Summary.unfreeze_summaries fs; global_env := newenv; kn diff --git a/library/global.mli b/library/global.mli index f0daef0ac..deafacba2 100644 --- a/library/global.mli +++ b/library/global.mli @@ -66,12 +66,13 @@ val set_engagement : engagement -> unit of the started module / module type *) val start_module : identifier -> module_path -val end_module : identifier -> module_struct_entry option -> module_path +val end_module : + Summary.frozen -> identifier -> module_struct_entry option -> module_path val add_module_parameter : mod_bound_id -> module_struct_entry -> unit val start_modtype : identifier -> module_path -val end_modtype : identifier -> module_path +val end_modtype : Summary.frozen -> identifier -> module_path diff --git a/library/goptions.ml b/library/goptions.ml index 6e58fd218..bf431e1fc 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -83,9 +83,7 @@ module MakeTable = Summary.declare_summary nick { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = true } + Summary.init_function = init } let (add_option,remove_option) = if A.synchronous then @@ -244,11 +242,9 @@ let declare_option cast uncast classify_function = (fun _ -> Dispose)} in let _ = declare_summary (nickname key) - {freeze_function = read; + { freeze_function = read; unfreeze_function = write; - init_function = (fun () -> write default); - survive_module = false; - survive_section = false} + init_function = (fun () -> write default) } in fun v -> add_anonymous_leaf (decl_obj v) else write diff --git a/library/heads.ml b/library/heads.ml index ba3a45594..c63634458 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -54,9 +54,7 @@ let _ = Summary.declare_summary "Head_decl" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = true; - Summary.survive_section = false } + Summary.init_function = init } let variable_head id = Evalrefmap.find (EvalVarRef id) !head_map let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map diff --git a/library/impargs.ml b/library/impargs.ml index 68809d6aa..aedb2d5a8 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -598,6 +598,4 @@ let _ = Summary.declare_summary "implicits" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } diff --git a/library/lib.ml b/library/lib.ml index c033a3805..1a3a07e01 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -519,9 +519,7 @@ let _ = Summary.declare_summary "section-context" { Summary.freeze_function = freeze_sectab; Summary.unfreeze_function = unfreeze_sectab; - Summary.init_function = init_sectab; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init_sectab } (*************) (* Sections. *) @@ -576,7 +574,7 @@ let close_section () = add_entry oname (ClosedSection (List.rev_append secdecls (List.rev secopening))); if !Flags.xml_export then !xml_close_section (basename (fst oname)); let newdecls = List.map discharge_item secdecls in - Summary.section_unfreeze_summaries fs; + Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; Cooking.clear_cooking_sharing (); Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) diff --git a/library/library.ml b/library/library.ml index 24c2c3803..831687723 100644 --- a/library/library.ml +++ b/library/library.ml @@ -180,9 +180,7 @@ let _ = Summary.declare_summary "MODULES" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } (* various requests to the tables *) diff --git a/library/nametab.ml b/library/nametab.ml index 797f88e39..074386417 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -548,9 +548,7 @@ let _ = Summary.declare_summary "names" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } (* Deprecated synonyms *) diff --git a/library/summary.ml b/library/summary.ml index 145ce9e00..784d79d87 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -14,9 +14,7 @@ open Util type 'a summary_declaration = { freeze_function : unit -> 'a; unfreeze_function : 'a -> unit; - init_function : unit -> unit; - survive_module : bool ; - survive_section : bool } + init_function : unit -> unit } let summaries = (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t) @@ -29,9 +27,7 @@ let internal_declare_summary sumname sdecl = let ddecl = { freeze_function = dyn_freeze; unfreeze_function = dyn_unfreeze; - init_function = dyn_init; - survive_module = sdecl.survive_module; - survive_section = sdecl.survive_section } + init_function = dyn_init } in if Hashtbl.mem summaries sumname then anomalylabstrm "Summary.declare_summary" @@ -51,23 +47,12 @@ let freeze_summaries () = !m -let unfreeze_some_summaries p fs = +let unfreeze_summaries fs = Hashtbl.iter (fun id decl -> - try - if p decl then - decl.unfreeze_function (Stringmap.find id fs) + try decl.unfreeze_function (Stringmap.find id fs) with Not_found -> decl.init_function()) summaries -let unfreeze_summaries = - unfreeze_some_summaries (fun _ -> true) - -let section_unfreeze_summaries = - unfreeze_some_summaries (fun decl -> not decl.survive_section) - -let module_unfreeze_summaries = - unfreeze_some_summaries (fun decl -> not decl.survive_module) - let init_summaries () = Hashtbl.iter (fun _ decl -> decl.init_function()) summaries diff --git a/library/summary.mli b/library/summary.mli index 3e6375b0e..e6e17ef8c 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -14,9 +14,7 @@ type 'a summary_declaration = { freeze_function : unit -> 'a; unfreeze_function : 'a -> unit; - init_function : unit -> unit; - survive_module : bool; (* should be false is most cases *) - survive_section : bool } + init_function : unit -> unit } val declare_summary : string -> 'a summary_declaration -> unit @@ -24,8 +22,6 @@ type frozen val freeze_summaries : unit -> frozen val unfreeze_summaries : frozen -> unit -val section_unfreeze_summaries : frozen -> unit -val module_unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit (** Beware: if some code is dynamically loaded via dynlink after the diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 6ce6c2c09..87e8e1deb 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -302,6 +302,4 @@ let _ = declare_summary "GRAMMAR_LEXER" { freeze_function = freeze; unfreeze_function = unfreeze; - init_function = init; - survive_module = false; - survive_section = false } + init_function = init } diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index 3a408909d..17d41ee8b 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -203,9 +203,7 @@ let () = { Summary.freeze_function = (fun () -> !globals, !globals_stack); Summary.unfreeze_function = (fun (g,s) -> globals := g; globals_stack := s); - Summary.init_function = (fun () -> ()); - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = (fun () -> ()) } let add_global r d = globals := Refmap.add r d !globals let mem_global r = Refmap.mem r !globals @@ -986,6 +984,4 @@ let _ = declare_summary "Dp options" init_function = (fun () -> debug := false; trace := false; timeout := 10; - prelude_files := []); - survive_module = true; - survive_section = true } + prelude_files := []) } diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index e6d634466..7a265b526 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -421,9 +421,7 @@ let (extr_lang,_) = let _ = declare_summary "Extraction Lang" { freeze_function = (fun () -> !lang_ref); unfreeze_function = ((:=) lang_ref); - init_function = (fun () -> lang_ref := Ocaml); - survive_module = true; - survive_section = true } + init_function = (fun () -> lang_ref := Ocaml) } let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) @@ -460,9 +458,7 @@ let (inline_extraction,_) = let _ = declare_summary "Extraction Inline" { freeze_function = (fun () -> !inline_table); unfreeze_function = ((:=) inline_table); - init_function = (fun () -> inline_table := empty_inline_table); - survive_module = true; - survive_section = true } + init_function = (fun () -> inline_table := empty_inline_table) } (* Grammar entries. *) @@ -542,9 +538,7 @@ let (blacklist_extraction,_) = let _ = declare_summary "Extraction Blacklist" { freeze_function = (fun () -> !blacklist_table); unfreeze_function = ((:=) blacklist_table); - init_function = (fun () -> blacklist_table := Idset.empty); - survive_module = true; - survive_section = true } + init_function = (fun () -> blacklist_table := Idset.empty) } (* Grammar entries. *) @@ -603,9 +597,7 @@ let (in_customs,_) = let _ = declare_summary "ML extractions" { freeze_function = (fun () -> !customs); unfreeze_function = ((:=) customs); - init_function = (fun () -> customs := Refmap.empty); - survive_module = true; - survive_section = true } + init_function = (fun () -> customs := Refmap.empty) } (* Grammar entries. *) diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 916294774..7401491e4 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -56,9 +56,7 @@ let _ = Summary.declare_summary "field" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } let load_addfield _ = () let cache_addfield (_,(typ,th)) = th_tab := Gmap.add typ th !th_tab diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 868a876be..3583c8448 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -434,9 +434,7 @@ let _ = Summary.declare_summary "functions_db_sum" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } let find_or_none id = try Some diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index a07ec4757..2ed20b2bb 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -181,9 +181,7 @@ let _ = Summary.declare_summary "tactic-ring-table" { Summary.freeze_function = (fun () -> !theories_map); Summary.unfreeze_function = (fun t -> theories_map := t); - Summary.init_function = (fun () -> theories_map := Cmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = (fun () -> theories_map := Cmap.empty) } (* declare a new type of object in the environment, "tactic-ring-theory" The functions theory_to_obj and obj_to_theory do the conversions diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 24cb84ed5..14fd9192e 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -389,9 +389,7 @@ let _ = Summary.init_function = (fun () -> from_carrier := Cmap.empty; from_relation := Cmap.empty; - from_name := Spmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + from_name := Spmap.empty) } let add_entry (sp,_kn) e = (* let _ = ty e.ring_lemma1 in @@ -971,9 +969,7 @@ let _ = Summary.init_function = (fun () -> field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty; - field_from_name := Spmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + field_from_name := Spmap.empty) } let add_field_entry (sp,_kn) e = (* diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index a8f5815bc..74ac78706 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -142,9 +142,7 @@ let _ = Summary.declare_summary "program-tcc-table" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } let progmap_union = ProgMap.fold ProgMap.add diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 901341e7b..348ae46dc 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -110,9 +110,7 @@ let _ = Summary.declare_summary "inh_graph" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } let _ = init() diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index c82589b9a..c29895912 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -125,9 +125,7 @@ let _ = declare_summary "record-methods-state" { freeze_function = (fun () -> !meth_dnet); unfreeze_function = (fun m -> meth_dnet := m); - init_function = (fun () -> meth_dnet := MethodsDnet.empty); - survive_module = false; - survive_section = false } + init_function = (fun () -> meth_dnet := MethodsDnet.empty) } open Libobject @@ -333,6 +331,4 @@ let _ = Summary.declare_summary "objdefs" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 1c7cfa9f6..fc790c672 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -140,9 +140,7 @@ let _ = Summary.declare_summary "evaluation" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } (* [compute_consteval] determines whether c is an "elimination constant" diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 52e2eb24e..2e4f978f5 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -95,9 +95,7 @@ let _ = Summary.declare_summary "classes_and_instances" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = true } + Summary.init_function = init } let add_instance_hint_ref = ref (fun id pri -> assert false) let register_add_instance_hint = diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 2e10a9f4a..8efc26631 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -108,9 +108,7 @@ let _ = Summary.declare_summary "Transparent constants and variables" { Summary.freeze_function = Conv_oracle.freeze; Summary.unfreeze_function = Conv_oracle.unfreeze; - Summary.init_function = Conv_oracle.init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = Conv_oracle.init } (* Generic reduction: reduction functions used in reduction tactics *) diff --git a/tactics/auto.ml b/tactics/auto.ml index b998daa74..c62824d4b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -235,9 +235,7 @@ let unfreeze fs = searchtable := fs let _ = Summary.declare_summary "search" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } (**************************************************************************) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 63481abde..0d5a4ba25 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -73,9 +73,7 @@ let _ = Summary.declare_summary "autorewrite" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } let find_base bas = try Stringmap.find bas !rewtab diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index be4343b4f..c28a87f0e 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -191,9 +191,7 @@ let _ = Summary.declare_summary "destruct-hyp-concl" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } let forward_subst_tactic = ref (fun _ -> failwith "subst_tactic is not installed for DHyp") diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index c6c9bdd10..f03084d4d 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -427,9 +427,7 @@ let _ = declare_summary "transitivity-steps" { freeze_function = freeze; unfreeze_function = unfreeze; - init_function = init; - survive_module = false; - survive_section = false } + init_function = init } (* Main entry points *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e79174c66..9da5678cf 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -229,9 +229,7 @@ let _ = Summary.declare_summary "tactic-definition" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } (* Tactics table (TacExtend). *) diff --git a/test-suite/bugs/closed/shouldsucceed/335.v b/test-suite/bugs/closed/shouldsucceed/335.v new file mode 100644 index 000000000..166fa7a9f --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/335.v @@ -0,0 +1,5 @@ +(* Compatibility of Require with backtracking at interactive module end *) + +Module A. +Require List. +End A. diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index ae4e8cf52..5df33d459 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id:$ i*) +(*i $Id$ i*) open Names open Mod_subst @@ -24,9 +24,7 @@ let export_scheme obj = let _ = Summary.declare_summary "eqscheme" { Summary.freeze_function = (fun () -> !eq_scheme_map); Summary.unfreeze_function = (fun fs -> eq_scheme_map := fs); - Summary.init_function = (fun () -> eq_scheme_map := Indmap.empty); - Summary.survive_module = false; - Summary.survive_section = true} + Summary.init_function = (fun () -> eq_scheme_map := Indmap.empty) } let find_eq_scheme ind = Indmap.find ind !eq_scheme_map @@ -62,9 +60,7 @@ let export_dec_proof obj = let _ = Summary.declare_summary "bl_proof" { Summary.freeze_function = (fun () -> !bl_map); Summary.unfreeze_function = (fun fs -> bl_map := fs); - Summary.init_function = (fun () -> bl_map := Indmap.empty); - Summary.survive_module = false; - Summary.survive_section = true} + Summary.init_function = (fun () -> bl_map := Indmap.empty) } let find_bl_proof ind = Indmap.find ind !bl_map @@ -75,9 +71,7 @@ let check_bl_proof ind = let _ = Summary.declare_summary "lb_proof" { Summary.freeze_function = (fun () -> !lb_map); Summary.unfreeze_function = (fun fs -> lb_map := fs); - Summary.init_function = (fun () -> lb_map := Indmap.empty); - Summary.survive_module = false; - Summary.survive_section = true} + Summary.init_function = (fun () -> lb_map := Indmap.empty) } let find_lb_proof ind = Indmap.find ind !lb_map @@ -88,9 +82,7 @@ let check_lb_proof ind = let _ = Summary.declare_summary "eq_dec_proof" { Summary.freeze_function = (fun () -> !dec_map); Summary.unfreeze_function = (fun fs -> dec_map := fs); - Summary.init_function = (fun () -> dec_map := Indmap.empty); - Summary.survive_module = false; - Summary.survive_section = true} + Summary.init_function = (fun () -> dec_map := Indmap.empty) } let find_eq_dec_proof ind = Indmap.find ind !dec_map diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index 4e10d1d52..c999c0609 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -51,9 +51,7 @@ let _ = declare_summary "type-library-state" { freeze_function = freeze; unfreeze_function = unfreeze; - init_function = init; - survive_module = false; - survive_section = false } + init_function = init } let load (_,d) = (* Profile.print_logical_stats !all_types; diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 837d50207..c390c7c52 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -274,9 +274,7 @@ let _ = Summary.declare_summary "ML-MODULES" { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules())); Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x); - Summary.init_function = (fun () -> init_ml_modules ()); - Summary.survive_module = false; - Summary.survive_section = true } + Summary.init_function = (fun () -> init_ml_modules ()) } (* Same as restore_ml_modules, but verbosely *) |