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

13 files changed, 32 insertions, 78 deletions

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