From 79a25a71dd3519d8e7a6bd9f3a004c7c0da3a1b5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 13 Aug 2009 19:10:11 +0000 Subject: Death of "survive_module" and "survive_section" (the first one was only used to allow a module to be ended before the summaries were restored what can be solved by moving upwards the place where the summaries are restored). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/summary.ml | 23 ++++------------------- 1 file changed, 4 insertions(+), 19 deletions(-) (limited to 'library/summary.ml') 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 -- cgit v1.2.3