From 27a87e4487c8b926aa0ed6c0ab65333d4ef5c3bc Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 2 Apr 2015 13:16:17 +0200
Subject: Display the proper error message when Require fails to find a
 library.

---
 toplevel/vernacentries.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7d29a3f8e0..5d4f5a4618 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
-- 
cgit v1.2.3