aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh6
-rw-r--r--interp/constrexpr_ops.ml5
-rw-r--r--interp/constrintern.ml35
-rw-r--r--interp/modintern.ml9
-rw-r--r--interp/notation.ml46
-rw-r--r--interp/smartlocate.ml8
-rw-r--r--kernel/cbytegen.ml7
-rw-r--r--lib/cErrors.ml11
-rw-r--r--lib/cErrors.mli4
-rw-r--r--library/nametab.ml16
-rw-r--r--library/nametab.mli2
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/ltac/tacintern.ml39
-rw-r--r--plugins/ltac/tacinterp.ml19
-rw-r--r--pretyping/coercion.ml50
-rw-r--r--pretyping/pretype_errors.ml10
-rw-r--r--pretyping/pretype_errors.mli2
-rw-r--r--user-contrib/Ltac2/tac2core.ml5
-rw-r--r--vernac/obligations.ml12
-rw-r--r--vernac/record.ml14
20 files changed, 195 insertions, 107 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 d6097304ec..ea27870535 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..af84e85d8e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -164,8 +164,8 @@ 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 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 =
@@ -1086,7 +1086,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 +1172,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
@@ -1810,20 +1816,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(loc,NotAConstructor _) as exn ->
+ let _, info = Exninfo.capture exn in
+ error_bad_inductive_type ?loc ~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 *)
@@ -2385,9 +2393,10 @@ 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)
-
+ InternalizationError (loc,e) as exn ->
+ (* XXX: use regular printer? *)
+ let _, info = Exninfo.capture exn in
+ user_err ?loc ~info ~hdr:"internalize" (explain_internalization_error e)
(*********************************************************************)
(* Functions to parse and interpret constructions *)
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 fb3cefd624..cd2df58ed4 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
@@ -1031,12 +1036,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 *)
@@ -1158,8 +1168,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)
@@ -1192,9 +1203,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 6d350ade8d..5e8babbf80 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))
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:13:23 +0000