From 4d89c31ff0a60e93e2a301f32d1e02f035eafaa2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 12 Oct 2002 14:28:47 +0000
Subject: Forcer la réouverture d'un fichier explicitement requis même si le
 fichier a déjà été ouvert précédemment (peut-être indirectement) par un autre
 Require.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3115 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/library.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/library/library.ml b/library/library.ml
index 8dd3c54322..c7f3ba4330 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -256,8 +256,15 @@ let segment_iter i v f =
 (*let open_objects i decls =
   segment_iter i (Exactly i) open_object decls*)
 
-let open_library export m =
-  if not (library_is_opened m.library_name) then begin
+let eq_lib_name m1 m2 = m1.library_name = m2.library_name
+
+let open_library export explicit_libs m =
+  if
+    (* Only libraries indirectly to open are not reopen *)
+    (* Libraries explicitly mentionned by the user are always reopen *)
+    List.exists (eq_lib_name m) explicit_libs
+    or not (library_is_opened m.library_name)
+  then begin
     register_open_library export m;
     Declaremods.import_module (MPfile m.library_name)
   end
@@ -275,7 +282,7 @@ let open_libraries export modl =
              [] m.library_imports
          in remember_last_of_each subimport m)
       [] modl in
-  List.iter (open_library export) to_open_list
+  List.iter (open_library export modl) to_open_list
 
 
 (************************************************************************)
-- 
cgit v1.2.3