From X Require Y looks for X with absolute path, disregarding -R.

1 files changed, 18 insertions, 6 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 62e5f0a324..7d29a3f8e0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -392,7 +392,7 @@ let err_notfound_library loc qid =
 
 let print_located_library r =
   let (loc,qid) = qualid_of_reference r in
-  try msg_found_library (Library.locate_qualified_library false qid)
+  try msg_found_library (Library.locate_qualified_library ~warn:false qid)
   with
     | Library.LibUnmappedDir -> err_unmapped_library loc qid
     | Library.LibNotFound -> err_notfound_library loc qid
@@ -750,12 +750,24 @@ let vernac_end_segment (_,id as lid) =
 (* Libraries *)
 
 let vernac_require from import qidl =
-  let qidl = match from with
-  | None -> qidl
-  | Some ns -> List.map (Libnames.join_reference ns) qidl
-  in
   let qidl = List.map qualid_of_reference qidl in
-  let modrefl = List.map Library.try_locate_qualified_library qidl in
+  let root = match from with
+  | None -> None
+  | Some from ->
+    let (_, qid) = Libnames.qualid_of_reference from in
+    let (hd, tl) = Libnames.repr_qualid qid in
+    Some (Libnames.add_dirpath_suffix hd tl)
+  in
+  let locate (loc, qid) =
+    try
+      let warn = Flags.is_verbose () in
+      let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in
+      (dir, f)
+    with
+      | Library.LibUnmappedDir -> err_unmapped_library loc qid
+      | Library.LibNotFound -> err_unmapped_library loc qid
+  in
+  let modrefl = List.map locate qidl in
   if Dumpglob.dump () then
     List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
   Library.require_library_from_dirpath modrefl import