From f4ee7ee31e4bc4a49de784d90b331abd3a21e34f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 21 Feb 2015 20:10:26 +0100
Subject: Fixing 934761875 about optimizing Import of several libraries at once
 (thanks to Enrico for noticing a bug).

---
 library/library.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'library/library.ml')

diff --git a/library/library.ml b/library/library.ml
index e4169d66e..95b817d0a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -587,8 +587,11 @@ let import_module export modl =
     | [] -> ()
     | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
   let rec aux acc = function
-    | m :: l ->
-        (match safe_locate_module m with
+    | (loc,dir as m) :: l ->
+        let m,acc =
+          try Nametab.locate_module dir, acc
+          with Not_found-> flush acc; safe_locate_module m, [] in
+        (match m with
         | MPfile dir -> aux (dir::acc) l
         | mp -> flush acc; Declaremods.import_module export mp; aux [] l)
     | [] -> flush acc
-- 
cgit v1.2.3