diff options
| author | Maxime Dénès | 2018-03-10 10:04:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-10 10:04:56 +0100 |
| commit | 4d5c7243b4aea5b28358757e2d86c11334da6699 (patch) | |
| tree | ade1ab73a9c2066302145bb3781a39b5d46b4513 /library/library.ml | |
| parent | 93a1c4786c9b17efdda025f754ad97376d61a9ba (diff) | |
| parent | b1d749e59444f86e40f897c41739168bb1b1b9b3 (diff) | |
Merge PR #6837: [located] Push inner locations in reference to a CAst.t node.
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/library.ml b/library/library.ml index fb9b54462e..56d2709d5b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -577,7 +577,7 @@ let require_library_from_dirpath modrefl export = (* the function called by Vernacentries.vernac_import *) -let safe_locate_module (loc,qid) = +let safe_locate_module {CAst.loc;v=qid} = try Nametab.locate_module qid with Not_found -> user_err ?loc ~hdr:"import_library" @@ -595,7 +595,7 @@ let import_module export modl = | [] -> () | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in let rec aux acc = function - | (loc, dir as m) :: l -> + | ({CAst.loc; v=dir} as m) :: l -> let m,acc = try Nametab.locate_module dir, acc with Not_found-> flush acc; safe_locate_module m, [] in |