Correction de l'ordre des open (sachant que de toutes façons, un

Require au milieu d'un module sera considéré comme situé au début du
module chargé)


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

1 files changed, 6 insertions, 5 deletions

diff --git a/library/library.ml b/library/library.ml
index 5d0a2a5ff..bba4ae35c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -268,11 +268,12 @@ let open_modules export modl =
   let to_open_list = 
     List.fold_left
       (fun l m ->
-         List.fold_left (fun l m -> 
-                           let m = find_module m in
-                           remember_last_of_each l m)
-           (remember_last_of_each l m)
-           m.module_imports) [] modl in
+         let subimport =
+           List.fold_left
+             (fun l m -> remember_last_of_each l (find_module m))
+             [] m.module_imports
+         in remember_last_of_each subimport m)
+      [] modl in
   List.iter (open_module export) to_open_list
 
 (*s [load_module s] loads the module [s] from the disk, and [find_module s]