From b4b790a773e2c9618b978ca89d27359344789009 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 24 Jan 2002 17:46:59 +0000
Subject: 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
---
 library/library.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/library/library.ml b/library/library.ml
index 5d0a2a5ff2..bba4ae35c3 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]
-- 
cgit v1.2.3