Meilleure approche du conflit path/freeze/library_root en séquentialisant la partie asynchrone (path) de la partie synchrone (roots)

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

1 files changed, 3 insertions, 6 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index 4e6b81d3b..b62f4d867 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -186,14 +186,11 @@ let exists_module sp =
 (********************************************************************)
 (* Registration of persistent tables as a global table and rollback *)
 
-(* Warning: We do not register roots, because otherwise option -R is
-   overwritten by the next input state *)
-
 type frozen = module_contents
 
-let init () = persistent_nametab := empty
-let freeze () = !persistent_nametab
-let unfreeze mc = persistent_nametab := mc
+let init () = persistent_nametab := empty; roots := []
+let freeze () = !persistent_nametab, !roots
+let unfreeze (mc,r) = persistent_nametab := mc; roots := r
 
 let _ = 
   Summary.declare_summary "persistent-names"