Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several

libraries at once (see #4193).

1 files changed, 6 insertions, 1 deletions

diff --git a/library/library.ml b/library/library.ml
index 9d0ccb972..b4261309f 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