diff options
| -rw-r--r-- | vernac/comCoercion.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 56ab6f289d..2c582da495 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -198,10 +198,9 @@ let build_id_coercion idf_opt source poly = lams in (* juste pour verification *) - let _ = - if not - (Reductionops.is_conv_leq env sigma - (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f)) + let sigma, val_t = Typing.type_of env sigma (EConstr.of_constr val_f) in + let () = + if not (Reductionops.is_conv_leq env sigma val_t (EConstr.of_constr typ_f)) then user_err (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") |