certains effets disparaissent a la sortie des sections, d'autres non (selon Summary.survive_section)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 1 deletions

diff --git a/library/library.ml b/library/library.ml
index da7d01895f..70cf895e53 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -54,7 +54,8 @@ let _ =
   Summary.declare_summary "MODULES"
     { Summary.freeze_function = (fun () -> !modules_table);
       Summary.unfreeze_function = (fun ft -> modules_table := ft);
-      Summary.init_function = (fun () -> modules_table := Stringmap.empty) }
+      Summary.init_function = (fun () -> modules_table := Stringmap.empty);
+      Summary.survive_section = true }
 
 let find_module s =
   try