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

Ack-by: SkySkimmer
Reviewed-by: ppedrot

20 files changed, 228 insertions, 137 deletions

diff --git a/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh b/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh
new file mode 100644
index 0000000000..05192facbe
--- /dev/null
+++ b/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11566" ] || [ "$CI_BRANCH" = "exninfo+coercion" ]; then
+
+    mtac2_CI_REF=exninfo+coercion
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index a8fb5a3f45..3d99e1d227 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -618,8 +618,9 @@ let interp_univ_constraints env evd cstrs =
     let cstrs' = Univ.Constraint.add cstr cstrs in
     try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
         evd, cstrs'
-    with Univ.UniverseInconsistency e ->
-      CErrors.user_err ~hdr:"interp_constraint"
+    with Univ.UniverseInconsistency e as exn ->
+      let _, info = Exninfo.capture exn in
+      CErrors.user_err ~hdr:"interp_constraint" ~info
         (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
   in
   List.fold_left interp (evd,Univ.Constraint.empty) cstrs
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5ad8af6d57..ee041ed088 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -115,7 +115,7 @@ type internalization_error =
   | NotAProjectionOf of qualid * qualid
   | ProjectionsOfDifferentRecords of qualid * qualid
 
-exception InternalizationError of internalization_error Loc.located
+exception InternalizationError of internalization_error
 
 let explain_variable_capture id id' =
   Id.print id ++ str " is dependent in the type of " ++ Id.print id' ++
@@ -164,8 +164,13 @@ let explain_internalization_error e =
     explain_projections_of_diff_records inductive1_id inductive2_id
   in pp ++ str "."
 
-let error_bad_inductive_type ?loc =
-  user_err ?loc  (str
+let _ = CErrors.register_handler (function
+    | InternalizationError e ->
+      Some (explain_internalization_error e)
+    | _ -> None)
+
+let error_bad_inductive_type ?loc ?info () =
+  user_err ?loc ?info (str
     "This should be an inductive type applied to patterns.")
 
 let error_parameter_not_implicit ?loc =
@@ -368,7 +373,7 @@ let impls_term_list n ?(args = []) =
 (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
 let rec check_capture ty = let open CAst in function
   | { loc; v = Name id } :: { v = Name id' } :: _ when occur_glob_constr id ty ->
-      raise (InternalizationError (loc,VariableCapture (id,id')))
+    Loc.raise ?loc (InternalizationError (VariableCapture (id,id')))
   | _::nal ->
       check_capture ty nal
   | [] ->
@@ -1086,7 +1091,9 @@ let intern_extended_global_of_qualid qid =
 let intern_reference qid =
   let r =
     try intern_extended_global_of_qualid qid
-    with Not_found -> Nametab.error_global_not_found qid
+    with Not_found as exn ->
+      let _, info = Exninfo.capture exn in
+      Nametab.error_global_not_found ~info qid
   in
   Smartlocate.global_of_extended_global r
 
@@ -1170,16 +1177,20 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
         let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
         check_applied_projection isproj realref qid;
         find_appl_head_data r, args2
-      with Not_found ->
+      with Not_found as exn ->
         (* Extra allowance for non globalizing functions *)
         if !interning_grammar || env.unb then
           (* check_applied_projection ?? *)
           (gvar (loc,qualid_basename qid) us, [], []), args
-        else Nametab.error_global_not_found qid
+        else
+          let _, info = Exninfo.capture exn in
+          Nametab.error_global_not_found ~info qid
   else
     let r,realref,args2 =
       try intern_qualid qid intern env ntnvars us args
-      with Not_found -> Nametab.error_global_not_found qid
+      with Not_found as exn ->
+        let _, info = Exninfo.capture exn in
+        Nametab.error_global_not_found ~info qid
     in
     check_applied_projection isproj realref qid;
     find_appl_head_data r, args2
@@ -1253,14 +1264,16 @@ let loc_of_lhs lhs =
 let check_linearity lhs ids =
   match has_duplicate ids with
     | Some id ->
-        raise (InternalizationError (loc_of_lhs lhs,NonLinearPattern id))
+      let loc = loc_of_lhs lhs in
+      Loc.raise ?loc (InternalizationError (NonLinearPattern id))
     | None ->
         ()
 
 (* Match the number of pattern against the number of matched args *)
 let check_number_of_pattern loc n l =
   let p = List.length l in
-  if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
+  if not (Int.equal n p) then
+    Loc.raise ?loc (InternalizationError (BadPatternsNumber (n,p)))
 
 let check_or_pat_variables loc ids idsl =
   let eq_id {v=id} {v=id'} = Id.equal id id' in
@@ -1392,7 +1405,7 @@ let find_constructor loc add_params ref =
 
 let find_pattern_variable qid =
   if qualid_is_ident qid then qualid_basename qid
-  else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid))
+  else Loc.raise ?loc:qid.CAst.loc (InternalizationError(NotAConstructor qid))
 
 let check_duplicate ?loc fields =
   let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in
@@ -1429,8 +1442,10 @@ let sort_fields ~complete loc fields completer =
             let gr = locate_reference first_field_ref in
             Dumpglob.add_glob ?loc:first_field_ref.CAst.loc gr;
             (gr, Recordops.find_projection gr)
-          with Not_found ->
-            raise (InternalizationError(first_field_ref.CAst.loc, NotAProjection first_field_ref))
+          with Not_found as exn ->
+            let _, info = Exninfo.capture exn in
+            let info = Option.cata (Loc.add_loc info) info loc in
+            Exninfo.iraise (InternalizationError(NotAProjection first_field_ref), info)
         in
         (* the number of parameters *)
         let nparams = record.Recordops.s_EXPECTEDPARAM in
@@ -1465,10 +1480,10 @@ let sort_fields ~complete loc fields completer =
                      try Recordops.find_projection field_glob_ref
                      with Not_found ->
                        let inductive_ref = inductive_of_record floc record in
-                       raise (InternalizationError(floc, NotAProjectionOf (field_ref, inductive_ref))) in
+                       Loc.raise ?loc:floc (InternalizationError(NotAProjectionOf (field_ref, inductive_ref))) in
                    let ind1 = inductive_of_record floc record in
                    let ind2 = inductive_of_record floc this_field_record in
-                   raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2)))
+                   Loc.raise ?loc (InternalizationError(ProjectionsOfDifferentRecords (ind1, ind2)))
                in
                if not regular && complete then
                  (* "regular" is false when the field is defined
@@ -1655,12 +1670,16 @@ let drop_notations_pattern looked_for genv =
       begin
         match drop_syndef top scopes head pl with
           | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
-          | None -> raise (InternalizationError (loc,NotAConstructor head))
+          | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head))
       end
     | CPatCstr (qid, Some expl_pl, pl) ->
-      let g = try Nametab.locate qid
-              with Not_found ->
-              raise (InternalizationError (loc,NotAConstructor qid)) in
+      let g =
+        try Nametab.locate qid
+        with Not_found as exn ->
+          let _, info = Exninfo.capture exn in
+          let info = Option.cata (Loc.add_loc info) info loc in
+          Exninfo.iraise (InternalizationError (NotAConstructor qid), info)
+      in
       if expl_pl == [] then
         (* Convention: (@r) deactivates all further implicit arguments and scopes *)
         DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
@@ -1810,20 +1829,22 @@ let intern_ind_pattern genv ntnvars scopes pat =
   let no_not =
     try
       drop_notations_pattern (function (GlobRef.IndRef _ | GlobRef.ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
-    with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc
+    with InternalizationError(NotAConstructor _) as exn ->
+      let _, info = Exninfo.capture exn in
+      error_bad_inductive_type ~info ()
   in
   let loc = no_not.CAst.loc in
   match DAst.get no_not with
     | RCPatCstr (head, expl_pl, pl) ->
-      let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
+      let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc ()) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
         (List.length expl_pl) pl in
       let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in
       (with_letin,
        match product_of_cases_patterns empty_alias idslpl with
        | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin)
-       | _ -> error_bad_inductive_type ?loc)
-    | x -> error_bad_inductive_type ?loc
+       | _ -> error_bad_inductive_type ?loc ())
+    | x -> error_bad_inductive_type ?loc ()
 
 (**********************************************************************)
 (* Utilities for application                                          *)
@@ -1899,8 +1920,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         let dl = Array.of_list dl in
         let n =
           try List.index0 Id.equal iddef lf
-          with Not_found ->
-            raise (InternalizationError (locid,UnboundFixName (false,iddef)))
+          with Not_found as exn ->
+            let _, info = Exninfo.capture exn in
+            let info = Option.cata (Loc.add_loc info) info locid in
+            Exninfo.iraise (InternalizationError (UnboundFixName (false,iddef)),info)
         in
         let env = restart_lambda_binders env in
         let idl_temp = Array.map
@@ -1942,8 +1965,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         let dl = Array.of_list dl in
         let n =
           try List.index0 Id.equal iddef lf
-          with Not_found ->
-            raise (InternalizationError (locid,UnboundFixName (true,iddef)))
+          with Not_found as exn ->
+            let _, info = Exninfo.capture exn in
+            let info = Option.cata (Loc.add_loc info) info locid in
+            Exninfo.iraise (InternalizationError (UnboundFixName (true,iddef)), info)
         in
         let env = restart_lambda_binders env in
         let idl_tmp = Array.map
@@ -2171,7 +2196,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         DAst.make ?loc @@
         GEvar (n, List.map (on_snd (intern_no_implicit env)) l)
     | CPatVar _ ->
-        raise (InternalizationError (loc,IllegalMetavariable))
+      Loc.raise ?loc (InternalizationError IllegalMetavariable)
     (* end *)
     | CSort s ->
         DAst.make ?loc @@
@@ -2337,12 +2362,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         (intern_no_implicit enva a) :: (intern_args env subscopes args)
 
   in
-  try
-    intern env c
-  with
-      InternalizationError (loc,e) ->
-        user_err ?loc ~hdr:"internalize"
-          (explain_internalization_error e)
+  intern env c
 
 (**************************************************************************)
 (* Functions to translate constr_expr into glob_constr                    *)
@@ -2382,12 +2402,7 @@ let intern_gen kind env sigma
 let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
 let intern_type env sigma c = intern_gen IsType env sigma c
 let intern_pattern globalenv patt =
-  try
-    intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
-  with
-      InternalizationError (loc,e) ->
-        user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
-
+  intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
@@ -2500,7 +2515,6 @@ let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
 
 let intern_context env impl_env binders =
-  try
   let lvar = (empty_ltac_sign, Id.Map.empty) in
   let ids =
     (* We assume all ids around are parts of the prefix of the current
@@ -2514,8 +2528,6 @@ let intern_context env impl_env binders =
               tmp_scope = None; scopes = []; impls = impl_env;
               binder_block_names = Some (Some AbsPi,ids)}, []) binders in
   (lenv.impls, List.map glob_local_binder_of_extended bl)
-  with InternalizationError (loc,e) ->
-    user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
 
 let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
   let open EConstr in
diff --git a/interp/modintern.ml b/interp/modintern.ml
index ae152e1c1c..50f90ebea7 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -22,14 +22,15 @@ exception ModuleInternalizationError of module_internalization_error
 
 type module_kind = Module | ModType | ModAny
 
-let error_not_a_module_loc kind loc qid =
+let error_not_a_module_loc ~info kind loc qid =
   let s = string_of_qualid qid in
   let e = match kind with
     | Module -> Modops.ModuleTypingError (Modops.NotAModule s)
     | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
     | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
   in
-  Loc.raise ?loc e
+  let info = Option.cata (Loc.add_loc info) info loc in
+  Exninfo.iraise (e,info)
 
 let error_application_to_not_path loc me =
   Loc.raise ?loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me))
@@ -57,7 +58,9 @@ let lookup_module_or_modtype kind qid =
       if kind == Module then raise Not_found;
       let mp = Nametab.locate_modtype qid in
       Dumpglob.dump_modref ?loc mp "mod"; (mp,ModType)
-    with Not_found -> error_not_a_module_loc kind loc qid
+    with Not_found as exn ->
+      let _, info = Exninfo.capture exn in
+      error_not_a_module_loc ~info kind loc qid
 
 let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 3f13476355..d4a44d9622 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -125,13 +125,14 @@ let declare_scope scope =
   with Not_found ->
     scope_map := String.Map.add scope empty_scope !scope_map
 
-let error_unknown_scope sc =
-  user_err ~hdr:"Notation"
+let error_unknown_scope ~info sc =
+  user_err ~hdr:"Notation" ~info
     (str "Scope " ++ str sc ++ str " is not declared.")
 
 let find_scope ?(tolerant=false) scope =
   try String.Map.find scope !scope_map
-  with Not_found ->
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
     if tolerant then
       (* tolerant mode to be turn off after deprecation phase *)
       begin
@@ -140,7 +141,7 @@ let find_scope ?(tolerant=false) scope =
         empty_scope
       end
     else
-      error_unknown_scope scope
+      error_unknown_scope ~info scope
 
 let check_scope ?(tolerant=false) scope =
   let _ = find_scope ~tolerant scope in ()
@@ -158,7 +159,9 @@ let normalize_scope sc =
     try
       let sc = String.Map.find sc !delimiters_map in
       let _ = String.Map.find sc !scope_map in sc
-    with Not_found -> error_unknown_scope sc
+    with Not_found as exn ->
+      let _, info = Exninfo.capture exn in
+      error_unknown_scope ~info sc
 
 (**********************************************************************)
 (* The global stack of scopes                                         *)
@@ -257,8 +260,10 @@ let remove_delimiters scope =
        try
          let _ = ignore (String.Map.find key !delimiters_map) in
          delimiters_map := String.Map.remove key !delimiters_map
-       with Not_found ->
-         assert false (* A delimiter for scope [scope] should exist *)
+       with Not_found as exn ->
+         let _, info = Exninfo.capture exn in
+         (* XXX info *)
+         CErrors.anomaly ~info (str "A delimiter for scope [scope] should exist")
 
 let find_delimiters_scope ?loc key =
   try String.Map.find key !delimiters_map
@@ -1123,12 +1128,17 @@ let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
 
 let check_required_module ?loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
-  with Not_found ->
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
     match d with
-    | [] -> user_err ?loc ~hdr:"prim_token_interpreter"
-       (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.")
-    | _ -> user_err ?loc ~hdr:"prim_token_interpreter"
-       (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
+    | [] ->
+      user_err ?loc ~info ~hdr:"prim_token_interpreter"
+        (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++
+         str " could not be found in the current environment.")
+    | _ ->
+      user_err ?loc ~info ~hdr:"prim_token_interpreter"
+        (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++
+         str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
@@ -1250,8 +1260,9 @@ let interp_prim_token_gen ?loc g p local_scopes =
   try
     let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in
     pat, (loc,sc)
-  with Not_found ->
-    user_err ?loc ~hdr:"interp_prim_token"
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    user_err ?loc ~info ~hdr:"interp_prim_token"
     ((match p with
       | Numeral _ ->
          str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p)
@@ -1284,9 +1295,10 @@ let interp_notation ?loc ntn local_scopes =
     let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in
     Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) n.not_deprecation;
     n.not_interp, (n.not_location, sc)
-  with Not_found ->
-    user_err ?loc
-    (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    user_err ?loc ~info
+      (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
 let uninterp_notations c =
   List.map_append (fun key -> keymap_find key !notations_key_table)
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 03977fcb4e..33d8aa6064 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -56,11 +56,15 @@ let global_inductive_with_alias qid  =
   | ref ->
       user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
         (pr_qualid qid ++ spc () ++ str "is not an inductive type.")
-  with Not_found -> Nametab.error_global_not_found qid
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    Nametab.error_global_not_found ~info qid
 
 let global_with_alias ?head qid =
   try locate_global_with_alias ?head qid
-  with Not_found -> Nametab.error_global_not_found qid
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    Nametab.error_global_not_found ~info qid
 
 let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
   | AN r ->
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 050f986367..b3a4bd7471 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -874,8 +874,11 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
     (if !dump_bytecode then
       Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
-  with TooLargeInductive msg ->
-    let fn = if fail_on_error then CErrors.user_err ?loc:None ~hdr:"compile" else
+  with TooLargeInductive msg as exn ->
+    let _, info = Exninfo.capture exn in
+    let fn = if fail_on_error then
+        CErrors.user_err ?loc:None ~info ~hdr:"compile"
+      else
         (fun x -> Feedback.msg_warning x) in
     fn msg; None
 
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 62d465c703..cb64e36755 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -25,12 +25,17 @@ let _ =
   in
   Printexc.register_printer pr
 
-let anomaly ?loc ?label pp =
-  Loc.raise ?loc (Anomaly (label, pp))
+let anomaly ?loc ?info ?label pp =
+  let info = Option.default Exninfo.null info in
+  let info = Option.cata (Loc.add_loc info) info loc in
+  Exninfo.iraise (Anomaly (label, pp), info)
 
 exception UserError of string option * Pp.t (* User errors *)
 
-let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm))
+let user_err ?loc ?info ?hdr strm =
+  let info = Option.default Exninfo.null info in
+  let info = Option.cata (Loc.add_loc info) info loc in
+  Exninfo.iraise (UserError (hdr, strm), info)
 
 exception Timeout
 
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index 21d41c996d..cf1857cf04 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -21,7 +21,7 @@ val push : exn -> Exninfo.iexn
  [Anomaly] is used for system errors and [UserError] for the
    user's ones. *)
 
-val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a
+val anomaly : ?loc:Loc.t -> ?info:Exninfo.info -> ?label:string -> Pp.t -> 'a
 (** Raise an anomaly, with an optional location and an optional
     label identifying the anomaly. *)
 
@@ -34,7 +34,7 @@ exception UserError of string option * Pp.t
 (** Main error signaling exception. It carries a header plus a pretty printing
     doc *)
 
-val user_err : ?loc:Loc.t -> ?hdr:string -> Pp.t -> 'a
+val user_err : ?loc:Loc.t -> ?info:Exninfo.info -> ?hdr:string -> Pp.t -> 'a
 (** Main error raising primitive. [user_err ?loc ?hdr pp] signals an
     error [pp] with optional header and location [hdr] [loc] *)
 
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 } *)
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index f7d78551d8..a0627dbe63 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -581,7 +581,7 @@ let rec locate_ref = function
         with Nametab.GlobalizationError _ | UserError _ -> None
       in
       match mpo, ro with
-        | None, None -> Nametab.error_global_not_found qid
+        | None, None -> Nametab.error_global_not_found ~info:Exninfo.null qid
         | None, Some r -> let refs,mps = locate_ref l in r::refs,mps
         | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
         | Some mp, Some r ->
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 53dc518bd3..bcfdb5318e 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -97,13 +97,19 @@ let intern_global_reference ist qid =
   else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then
     let id = qualid_basename qid in
     ArgArg (qid.CAst.loc, GlobRef.VarRef id)
-  else match locate_global_with_alias ~head:true qid with
-  | r -> ArgArg (qid.CAst.loc, r)
-  | exception Not_found ->
-    if not !strict_check && qualid_is_ident qid then
-      let id = qualid_basename qid in
-      ArgArg (qid.CAst.loc, GlobRef.VarRef id)
-    else Nametab.error_global_not_found qid
+  else
+    let r =
+      try locate_global_with_alias ~head:true qid
+      with
+      | Not_found as exn ->
+        if not !strict_check && qualid_is_ident qid then
+          let id = qualid_basename qid in
+          GlobRef.VarRef id
+        else
+          let _, info = Exninfo.capture exn in
+          Nametab.error_global_not_found ~info qid
+    in
+    ArgArg (qid.CAst.loc, r)
 
 let intern_ltac_variable ist qid =
   if qualid_is_ident qid && find_var (qualid_basename qid) ist then
@@ -148,9 +154,10 @@ let intern_isolated_tactic_reference strict ist qid =
   with Not_found ->
   (* Tolerance for compatibility, allow not to use "constr:" *)
   try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid))
-  with Not_found ->
-  (* Reference not found *)
-  Nametab.error_global_not_found qid
+  with Not_found as exn ->
+    (* Reference not found *)
+    let _, info = Exninfo.capture exn in
+    Nametab.error_global_not_found ~info qid
 
 (* Internalize an applied tactic reference *)
 
@@ -167,9 +174,10 @@ let intern_applied_tactic_reference ist qid =
   with Not_found ->
   (* A global tactic *)
   try intern_applied_global_tactic_reference qid
-  with Not_found ->
-  (* Reference not found *)
-  Nametab.error_global_not_found qid
+  with Not_found as exn ->
+    (* Reference not found *)
+    let _, info = Exninfo.capture exn in
+    Nametab.error_global_not_found ~info qid
 
 (* Intern a reference parsed in a non-tactic entry *)
 
@@ -182,7 +190,7 @@ let intern_non_tactic_reference strict ist qid =
   with Not_found ->
   (* Tolerance for compatibility, allow not to use "ltac:" *)
   try intern_isolated_global_tactic_reference qid
-  with Not_found ->
+  with Not_found as exn ->
   (* By convention, use IntroIdentifier for unbound ident, when not in a def *)
   if qualid_is_ident qid && not strict then
     let id = qualid_basename qid in
@@ -190,7 +198,8 @@ let intern_non_tactic_reference strict ist qid =
     TacGeneric ipat
   else
     (* Reference not found *)
-    Nametab.error_global_not_found qid
+    let _, info = Exninfo.capture exn in
+    Nametab.error_global_not_found ~info qid
 
 let intern_message_token ist = function
   | (MsgString _ | MsgInt _ as x) -> x
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 5abe18e00c..97f7a198e6 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -378,7 +378,9 @@ let interp_reference ist env sigma = function
     with Not_found ->
       try
         GlobRef.VarRef (get_id (Environ.lookup_named id env))
-      with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
+      with Not_found as exn ->
+        let _, info = Exninfo.capture exn in
+        Nametab.error_global_not_found ~info (qualid_of_ident ?loc id)
 
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
@@ -391,17 +393,21 @@ let interp_evaluable ist env sigma = function
     (* Maybe [id] has been introduced by Intro-like tactics *)
     begin
       try try_interp_evaluable env (loc, id)
-      with Not_found ->
+      with Not_found as exn ->
         match r with
         | EvalConstRef _ -> r
-        | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
+        | _ ->
+          let _, info = Exninfo.capture exn in
+          Nametab.error_global_not_found ~info (qualid_of_ident ?loc id)
     end
   | ArgArg (r,None) -> r
   | ArgVar {loc;v=id} ->
     try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try try_interp_evaluable env (loc, id)
-      with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
+      with Not_found as exn ->
+        let _, info = Exninfo.capture exn in
+        Nametab.error_global_not_found ~info (qualid_of_ident ?loc id)
 
 (* Interprets an hypothesis name *)
 let interp_occurrences ist occs =
@@ -663,8 +669,9 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
         let c = coerce_to_closed_constr env x in
         Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
-     with Not_found ->
-       Nametab.error_global_not_found (qualid_of_ident ?loc id))
+     with Not_found as exn ->
+       let _, info = Exninfo.capture exn in
+       Nametab.error_global_not_found ~info (qualid_of_ident ?loc id))
   | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
   | Inr c -> Inr (interp_typed_pattern ist env sigma c) in
   interp_occurrences ist occs, p
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f931a32bf8..d759f82d35 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -146,8 +146,9 @@ let coerce ?loc env sigma (x : EConstr.constr) (y : EConstr.constr)
   let rec coerce_unify env sigma x y =
     let x = hnf env sigma x and y = hnf env sigma y in
     try
-      (Evarconv.unify_leq_delay env sigma x y, None)
-    with UnableToUnify _ -> coerce' env sigma x y
+      Evarconv.unify_leq_delay env sigma x y, None
+    with
+      Evarconv.UnableToUnify _ -> coerce' env sigma x y
   and coerce' env sigma x y : evar_map * (evar_map -> EConstr.constr -> evar_map * EConstr.constr) option =
     let subco sigma = subset_coerce env sigma x y in
     let dest_prod c =
@@ -165,16 +166,20 @@ let coerce ?loc env sigma (x : EConstr.constr) (y : EConstr.constr)
             let (n, eqT), restT = dest_prod typ in
             let (n', eqT'), restT' = dest_prod typ' in
             aux sigma (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
-          with UnableToUnify _ ->
+          with UnableToUnify _ as exn ->
+            let _, info = Exninfo.capture exn in
             let (n, eqT), restT = dest_prod typ in
             let (n', eqT'), restT' = dest_prod typ' in
             let sigma =
               try
                 unify_leq_delay env sigma eqT eqT'
-              with UnableToUnify _ -> raise NoSubtacCoercion
+              with UnableToUnify _ ->
+                let e, info = Exninfo.capture exn in
+                Exninfo.iraise (NoSubtacCoercion,info)
             in
             (* Disallow equalities on arities *)
-            if Reductionops.is_arity env sigma eqT then raise NoSubtacCoercion;
+            if Reductionops.is_arity env sigma eqT then
+              Exninfo.iraise (NoSubtacCoercion,info);
             let restargs = lift_args 1
                 (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
             in
@@ -448,7 +453,8 @@ let inh_app_fun_core ~program_mode env sigma j =
         try let t,p =
           lookup_path_to_fun_from env sigma j.uj_type in
             apply_coercion env sigma p j t
-       with Not_found | NoCoercion ->
+       with (Not_found | NoCoercion) as exn ->
+         let _, info = Exninfo.capture exn in
          if program_mode then
            try
              let sigma, (coercef, t, trace) = mu env sigma t in
@@ -457,7 +463,7 @@ let inh_app_fun_core ~program_mode env sigma j =
              (sigma, res, trace)
            with NoSubtacCoercion | NoCoercion ->
              (sigma,j,IdCoe)
-         else raise NoCoercion
+         else Exninfo.iraise (NoCoercion,info)
 
 (* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
 let inh_app_fun ~program_mode resolve_tc env sigma j =
@@ -523,7 +529,9 @@ let inh_coerce_to_fail flags env sigma rigidonly v t c1 =
       with Not_found -> raise NoCoercion
     in
     try (unify_leq_delay ~flags env sigma t' c1, v', trace)
-    with UnableToUnify _ -> raise NoCoercion
+    with Evarconv.UnableToUnify _ as exn ->
+      let _, info = Exninfo.capture exn in
+      Exninfo.iraise (NoCoercion,info)
 
 let default_flags_of env =
   default_flags_of TransparentState.full
@@ -532,7 +540,8 @@ let rec inh_conv_coerce_to_fail ?loc env sigma ?(flags=default_flags_of env) rig
   try (unify_leq_delay ~flags env sigma t c1, v, IdCoe)
   with UnableToUnify (best_failed_sigma,e) ->
     try inh_coerce_to_fail flags env sigma rigidonly v t c1
-    with NoCoercion ->
+    with NoCoercion as exn ->
+      let _, info = Exninfo.capture exn in
       match
       EConstr.kind sigma (whd_all env sigma t),
       EConstr.kind sigma (whd_all env sigma c1)
@@ -557,7 +566,8 @@ let rec inh_conv_coerce_to_fail ?loc env sigma ?(flags=default_flags_of env) rig
           let (sigma,v2',trace2) = inh_conv_coerce_to_fail ?loc env1 sigma rigidonly v2 t2 u2 in
           let trace = ProdCoe { na=name; ty=u1; dom=trace1; body=trace2 } in
           (sigma, mkLambda (name, u1, v2'), trace)
-      | _ -> raise (NoCoercionNoUnifier (best_failed_sigma,e))
+      | _ ->
+        Exninfo.iraise (NoCoercionNoUnifier (best_failed_sigma,e), info)
 
 (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
 let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env sigma cj t =
@@ -565,26 +575,30 @@ let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env sig
     try
       let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc env sigma ~flags rigidonly cj.uj_val cj.uj_type t in
       (sigma, val', Some trace)
-    with NoCoercionNoUnifier (best_failed_sigma,e) ->
+    with NoCoercionNoUnifier (best_failed_sigma,e) as exn ->
+      let _, info = Exninfo.capture exn in
       try
         if program_mode then
           let (sigma, val') = coerce_itf ?loc env sigma cj.uj_val cj.uj_type t in
           (sigma, val', None)
-        else raise NoSubtacCoercion
+        else Exninfo.iraise (NoSubtacCoercion,info)
       with
-      | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) ->
-          error_actual_type ?loc env best_failed_sigma cj t e
-      | NoSubtacCoercion ->
+      | NoSubtacCoercion as exn when not resolve_tc || not (get_use_typeclasses_for_conversion ()) ->
+        let _, info = Exninfo.capture exn in
+        error_actual_type ?loc ~info env best_failed_sigma cj t e
+      | NoSubtacCoercion as exn ->
+        let _, info = Exninfo.capture exn in
         let sigma' = saturate_evd env sigma in
           try
             if sigma' == sigma then
-              error_actual_type ?loc env best_failed_sigma cj t e
+              error_actual_type ?loc ~info env best_failed_sigma cj t e
             else
               let sigma = sigma' in
               let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc env sigma rigidonly cj.uj_val cj.uj_type t in
               (sigma, val', Some trace)
-          with NoCoercionNoUnifier (_sigma,_error) ->
-            error_actual_type ?loc env best_failed_sigma cj t e
+          with NoCoercionNoUnifier (_sigma,_error) as exn ->
+            let _, info = Exninfo.capture exn in
+            error_actual_type ?loc ~info env best_failed_sigma cj t e
   in
   (sigma,{ uj_val = val'; uj_type = t },otrace)
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 6994a7b78f..414663c826 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -69,15 +69,17 @@ let precatchable_exception = function
   | Nametab.GlobalizationError _ -> true
   | _ -> false
 
-let raise_pretype_error ?loc (env,sigma,te) =
-  Loc.raise ?loc (PretypeError(env,sigma,te))
+let raise_pretype_error ?loc ?info (env,sigma,te) =
+  let info = Option.default Exninfo.null info in
+  let info = Option.cata (Loc.add_loc info) info loc in
+  Exninfo.iraise (PretypeError(env,sigma,te),info)
 
 let raise_type_error ?loc (env,sigma,te) =
   Loc.raise ?loc (PretypeError(env,sigma,TypingError te))
 
-let error_actual_type ?loc env sigma {uj_val=c;uj_type=actty} expty reason =
+let error_actual_type ?loc ?info env sigma {uj_val=c;uj_type=actty} expty reason =
   let j = {uj_val=c;uj_type=actty} in
-  raise_pretype_error ?loc
+  raise_pretype_error ?loc ?info
     (env, sigma, ActualTypeNotCoercible (j, expty, reason))
 
 let error_actual_type_core ?loc env sigma {uj_val=c;uj_type=actty} expty =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 7086584642..70f218d617 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -75,7 +75,7 @@ val precatchable_exception : exn -> bool
 
 (** Raising errors *)
 val error_actual_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
+  ?loc:Loc.t -> ?info:Exninfo.info -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
       unification_error -> 'b
 
 val error_actual_type_core :
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index e77040a8db..0299da6a25 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1162,8 +1162,9 @@ let () =
   | Tac2qexpr.QReference qid ->
     let gr =
       try Nametab.locate qid
-      with Not_found ->
-        Nametab.error_global_not_found qid
+      with Not_found as exn ->
+        let _, info = Exninfo.capture exn in
+        Nametab.error_global_not_found ~info qid
     in
     GlbVal gr, gtypref t_reference
   in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5e746afc74..30ebf425d0 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,7 +20,7 @@ open DeclareObl
 open DeclareObl.Obligation
 open DeclareObl.ProgramDecl
 
-let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
+let pperror ?info cmd = CErrors.user_err ~hdr:"Program" ?info cmd
 let error s = pperror (str s)
 
 let reduce c =
@@ -92,10 +92,16 @@ let get_any_prog () =
   else raise (NoObligations None)
 
 let get_prog_err n =
-  try get_prog n with NoObligations id -> pperror (explain_no_obligations id)
+  try get_prog n
+  with NoObligations id as exn ->
+    let _, info = Exninfo.capture exn in
+    pperror ~info (explain_no_obligations id)
 
 let get_any_prog_err () =
-  try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id)
+  try get_any_prog ()
+  with NoObligations id as exn ->
+    let _, info = Exninfo.capture exn in
+    pperror ~info (explain_no_obligations id)
 
 let all_programs () =
   ProgMap.fold (fun k p l -> p :: l) (get_prg_info_map ()) []
diff --git a/vernac/record.ml b/vernac/record.ml
index 36254780cd..9d99036273 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -223,7 +223,7 @@ let warn_cannot_define_projection =
 (* If a projection is not definable, we throw an error if the user
 asked it to be a coercion. Otherwise, we just print an info
 message. The user might still want to name the field of the record. *)
-let warning_or_error coe indsp err =
+let warning_or_error ~info coe indsp err =
   let st = match err with
     | MissingProj (fi,projs) ->
         let s,have = if List.length projs > 1 then "s","were" else "","was" in
@@ -246,7 +246,7 @@ let warning_or_error coe indsp err =
           | _ ->
               (Id.print fi ++ strbrk " cannot be defined because it is not typable.")
   in
-  if coe then user_err ~hdr:"structure" st;
+  if coe then user_err ~hdr:"structure" ~info st;
   warn_cannot_define_projection (hov 0 st)
 
 type field_status =
@@ -352,8 +352,9 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
                let kind = Decls.IsDefinition kind in
                let kn =
                  try declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry)
-                 with Type_errors.TypeError (ctx,te) when not primitive ->
-                   raise (NotDefinable (BadTypedProj (fid,ctx,te)))
+                 with Type_errors.TypeError (ctx,te) as exn when not primitive ->
+                   let _, info = Exninfo.capture exn in
+                   Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info)
                in
                Declare.definition_message fid;
                let term = match p_opt with
@@ -374,8 +375,9 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
                end;
                let i = if is_local_assum decl then i+1 else i in
                (Some kn::sp_projs, i, Projection term::subst)
-             with NotDefinable why ->
-               warning_or_error flags.pf_subclass indsp why;
+             with NotDefinable why as exn ->
+               let _, info = Exninfo.capture exn in
+               warning_or_error ~info flags.pf_subclass indsp why;
                (None::sp_projs,i,NoProjection fi::subst)
          in
          (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst))