From f4ee7ee31e4bc4a49de784d90b331abd3a21e34f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
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')

diff --git a/library/library.ml b/library/library.ml
index e4169d66e0..95b817d0a1 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


From df2f50db3703b4f7f88f00ac382c7f3f1efaceb3 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 23 Feb 2015 11:26:51 +0100
Subject: Fix some typos in comments.

---
 library/assumptions.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/assumptions.mli b/library/assumptions.mli
index 809e536b43..bb36a97259 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -27,7 +27,7 @@ module ContextObjectMap : Map.ExtS
 (** Collects all the objects on which a term directly relies, bypassing kernel
     opacity, together with the recursive dependence DAG of objects.
 
-    WARNING: some terms may not make sense in the environement, because they are
+    WARNING: some terms may not make sense in the environment, because they are
     sealed inside opaque modules. Do not try to do anything fancy with those
     terms apart from printing them, otherwise demons may fly out of your nose.
 *)
-- 
cgit v1.2.3