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

5 files changed, 17 insertions, 10 deletions

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"
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8d45151b26..da86562f09 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -84,6 +84,9 @@ let init_load_path () =
   List.iter 
     (fun (s,alias,reci) ->
        if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias)
-    (List.rev !includes);
-  includes := []
+    (List.rev !includes)
 
+let init_library_roots () =
+  List.iter
+    (fun (_,alias,_) -> Nametab.push_library_root (List.hd alias)) !includes;
+  includes := []
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index a0b3d5911b..f81d88eae0 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -15,3 +15,4 @@ val push_include : string * Names.dir_path -> unit
 val push_rec_include : string * Names.dir_path -> unit
 
 val init_load_path : unit -> unit
+val init_library_roots : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5ece34630a..3d809508bd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -184,6 +184,7 @@ let start () =
       if is_verbose() then print_header ();
       init_load_path ();
       inputstate ();
+      init_library_roots ();
       load_vernac_obj ();
       require ();
       load_rcfile();
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9e53e01c4e..153e91667a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -198,10 +198,15 @@ let _ =
 	   let alias = Filename.basename dir in
 	   if alias = "" then
 	     error ("Cannot map "^dir^" to a root of Coq library");
-	   (fun () -> add_rec_path dir [alias])
+	   (fun () ->
+	      add_rec_path dir [alias];
+	      Nametab.push_library_root alias)
        | [VARG_STRING dir ; VARG_QUALID alias] ->
            let aliasdir,aliasname = repr_qualid alias in
-	    (fun () -> add_rec_path dir (aliasdir@[aliasname]))
+	    (fun () ->
+	       let alias = aliasdir@[aliasname] in
+	       add_rec_path dir alias;
+	       Nametab.push_library_root (List.hd alias))
        | _ -> bad_vernac_args "RECADDPATH")
 
 (* For compatibility *)