diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-02 13:16:17 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-02 14:14:16 +0200 |
| commit | 27a87e4487c8b926aa0ed6c0ab65333d4ef5c3bc (patch) | |
| tree | 5fe2cb6313f59d80c6343ec45204abca8eb63287 | |
| parent | 4de4ab77ab6d9bb72a41c3fee3920a4c1b7a9bbc (diff) | |
Display the proper error message when Require fails to find a library.
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7d29a3f8e..5d4f5a461 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -387,8 +387,9 @@ let err_unmapped_library loc qid = pr_dirpath dir ++ str".") let err_notfound_library loc qid = - msg_error - (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid ++ str".")) + user_err_loc + (loc,"locate_library", + strbrk "Unable to locate library " ++ pr_qualid qid ++ str".") let print_located_library r = let (loc,qid) = qualid_of_reference r in @@ -765,7 +766,7 @@ let vernac_require from import qidl = (dir, f) with | Library.LibUnmappedDir -> err_unmapped_library loc qid - | Library.LibNotFound -> err_unmapped_library loc qid + | Library.LibNotFound -> err_notfound_library loc qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then |