We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 4f65e9d commit e72fb38Copy full SHA for e72fb38
pretyping/coercion.ml
@@ -722,10 +722,10 @@ let inh_coerce_to_fail ?(use_coercions=true) flags env sigma rigidonly v v_ty ta
722
723
let rec inh_conv_coerce_to_fail ?loc ?use_coercions env sigma ?(flags=default_flags_of env) rigidonly v t c1 =
724
try (unify_leq_delay ~flags env sigma t c1, v, IdCoe)
725
- with UnableToUnify (best_failed_sigma,e) ->
+ with UnableToUnify (best_failed_sigma,e) as exn ->
726
+ let _, info = Exninfo.capture exn in
727
try inh_coerce_to_fail ?use_coercions flags env sigma rigidonly v t c1
- with NoCoercion as exn ->
728
- let _, info = Exninfo.capture exn in
+ with NoCoercion ->
729
match
730
EConstr.kind sigma (whd_all env sigma t),
731
EConstr.kind sigma (whd_all env sigma c1)
0 commit comments