From bc6787e51fdb3b2bb449d288791e963dd7416737 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Feb 2001 21:32:07 +0000
Subject: 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
---
 library/nametab.ml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'library')

diff --git a/library/nametab.ml b/library/nametab.ml
index 4e6b81d3b8..b62f4d867d 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"
-- 
cgit v1.2.3