Merge PR #11566: [misc] Better preserve backtraces in several modules

Ack-by: SkySkimmer
Reviewed-by: ppedrot

2 files changed, 11 insertions, 7 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index d9b4dc9122..a51c281f2b 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -43,8 +43,9 @@ end
 
 exception GlobalizationError of qualid
 
-let error_global_not_found qid =
-  Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid)
+let error_global_not_found ~info qid =
+  let info = Option.cata (Loc.add_loc info) info qid.CAst.loc in
+  Exninfo.iraise (GlobalizationError qid, info)
 
 (* The visibility can be registered either
    - for all suffixes not shorter then a given int - when the object
@@ -499,8 +500,9 @@ let global qid =
         user_err ?loc:qid.CAst.loc ~hdr:"global"
           (str "Unexpected reference to a notation: " ++
            pr_qualid qid)
-  with Not_found ->
-    error_global_not_found qid
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    error_global_not_found ~info qid
 
 (* Exists functions ********************************************************)
 
@@ -566,8 +568,10 @@ let shortest_qualid_of_universe ?loc kn =
 
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
-  with Not_found as e ->
-    if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
+  with Not_found as exn ->
+    let exn, info = Exninfo.capture exn in
+    if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found");
+    Exninfo.iraise (exn, info)
 
 let global_inductive qid =
   let open GlobRef in
diff --git a/library/nametab.mli b/library/nametab.mli
index 00cec35506..8a8b59733c 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -91,7 +91,7 @@ end
 exception GlobalizationError of qualid
 
 (** Raises a globalization error *)
-val error_global_not_found : qualid -> 'a
+val error_global_not_found : info:Exninfo.info -> qualid -> 'a
 
 (** {6 Register visibility of things } *)