diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-13 19:10:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-13 19:10:11 +0000 |
| commit | 79a25a71dd3519d8e7a6bd9f3a004c7c0da3a1b5 (patch) | |
| tree | 949401f9c40c65a0a6bb3f8aa14a97428649451a /library/summary.ml | |
| parent | 6366dec0a76dbaf100907b2d4cd4da84a2ba7fef (diff) | |
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
Diffstat (limited to 'library/summary.ml')
| -rw-r--r-- | library/summary.ml | 23 |
1 files changed, 4 insertions, 19 deletions
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 |