Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several

libraries at once (see #4193).

2 files changed, 13 insertions, 1 deletions

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).