diff options
| author | herbelin | 2002-10-12 14:28:47 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-12 14:28:47 +0000 |
| commit | 4d89c31ff0a60e93e2a301f32d1e02f035eafaa2 (patch) | |
| tree | 3e1f89639e354deac1463234110e0f90744e8e0b | |
| parent | a67e806a0626be0c6ed120e6fc534b5d1c5eaca7 (diff) | |
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
| -rw-r--r-- | library/library.ml | 13 |
1 files 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 (************************************************************************) |