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, 5 insertions, 5 deletions

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