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

1 files changed, 7 insertions, 15 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