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/nametab.ml b/library/nametab.ml
index c45e7d93e..de5c22c09 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -77,7 +77,8 @@ let _ =
   Summary.declare_summary "names"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = true }
 
 let rollback f x =
   let fs = freeze () in