diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c882d2108f..4d7300833a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -571,7 +571,7 @@ let vernac_end_segment lid = let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in - let modrefl = List.map (fun (_, qid) -> let (_, dp, _) = (Library.locate_qualified_library false qid) in dp) qidl in + let modrefl = List.map (fun qid -> let (dp, _) = (Library.try_locate_qualified_library qid) in dp) qidl in List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl modrefl; Library.require_library qidl import |