diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 62e5f0a32..7d29a3f8e 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 |