From 1c0a1dbfd13f0618b33213c4d42e50d44465c987 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 17 Apr 2015 15:36:11 +0200
Subject: Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of
 several libraries at once (see #4193).

---
 library/library.ml            | 7 ++++++-
 test-suite/bugs/closed/4193.v | 7 +++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4193.v

diff --git a/library/library.ml b/library/library.ml
index 9d0ccb972a..b4261309fd 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -633,7 +633,12 @@ let import_module export modl =
           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)
+        | mp ->
+            flush acc;
+            try Declaremods.import_module export mp; aux [] l
+            with Not_found ->
+              user_err_loc (loc,"import_library",
+                str ((string_of_qualid dir)^" is not a module")))
     | [] -> flush acc
   in aux [] modl
 
diff --git a/test-suite/bugs/closed/4193.v b/test-suite/bugs/closed/4193.v
new file mode 100644
index 0000000000..885d04a927
--- /dev/null
+++ b/test-suite/bugs/closed/4193.v
@@ -0,0 +1,7 @@
+Module Type E.
+End E.
+
+Module Type A (M : E).
+End A.
+
+Fail Module Type F (Import X : A).
-- 
cgit v1.2.3