Merge PR #18694: Use Loc.raise instead of raise in Require for missin…

…g libraries Reviewed-by: SkySkimmer Ack-by: ejgallego Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
coq · Feb 22, 2024 · f1e9816 · f1e9816
2 parents a36b8ce + e4efa55
commit f1e9816
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/test-suite/output/bug_15097.out b/test-suite/output/bug_15097.out
@@ -1,7 +1,7 @@
-File "./output/bug_15097.v", line 1, characters 0-39:
+File "./output/bug_15097.v", line 1, characters 20-38:
 The command has indeed failed with message:
 Cannot find a physical path bound to logical path Coq.Does.Not.Exist.
-File "./output/bug_15097.v", line 2, characters 0-44:
+File "./output/bug_15097.v", line 2, characters 29-43:
 The command has indeed failed with message:
 Cannot find a physical path bound to logical path
 Does.Not.Exist with prefix Coq.
diff --git a/vernac/synterp.ml b/vernac/synterp.ml
@@ -293,8 +293,8 @@ let synterp_require from export qidl =
     let open Loadpath in
     match locate_qualified_library ?root qid with
     | Ok (dir,_) -> dir
-    | Error LibUnmappedDir -> raise (UnmappedLibrary (root, qid))
-    | Error LibNotFound -> raise (NotFoundLibrary (root, qid))
+    | Error LibUnmappedDir -> Loc.raise ?loc:qid.loc (UnmappedLibrary (root, qid))
+    | Error LibNotFound -> Loc.raise ?loc:qid.loc (NotFoundLibrary (root, qid))
   in
   let modrefl = List.map locate qidl in
   let lib_resolver = Loadpath.try_locate_absolute_library in