diff options
-rw-r--r-- | library/library.ml | 7 | ||||
-rw-r--r-- | test-suite/bugs/closed/4193.v | 7 |
2 files changed, 13 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 diff --git a/test-suite/bugs/closed/4193.v b/test-suite/bugs/closed/4193.v new file mode 100644 index 000000000..885d04a92 --- /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). |