Skip to content

Commit 4043e70

Browse files
Merge PR #20665: Fix backtrace of exception reraised in coercion handling
Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
2 parents d8cde75 + e72fb38 commit 4043e70

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

pretyping/coercion.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -722,10 +722,10 @@ let inh_coerce_to_fail ?(use_coercions=true) flags env sigma rigidonly v v_ty ta
722722

723723
let rec inh_conv_coerce_to_fail ?loc ?use_coercions env sigma ?(flags=default_flags_of env) rigidonly v t c1 =
724724
try (unify_leq_delay ~flags env sigma t c1, v, IdCoe)
725-
with UnableToUnify (best_failed_sigma,e) ->
725+
with UnableToUnify (best_failed_sigma,e) as exn ->
726+
let _, info = Exninfo.capture exn in
726727
try inh_coerce_to_fail ?use_coercions flags env sigma rigidonly v t c1
727-
with NoCoercion as exn ->
728-
let _, info = Exninfo.capture exn in
728+
with NoCoercion ->
729729
match
730730
EConstr.kind sigma (whd_all env sigma t),
731731
EConstr.kind sigma (whd_all env sigma c1)

0 commit comments

Comments
 (0)