diff options
| author | Gaëtan Gilbert | 2020-02-06 17:35:47 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 15387f4e32d7eac580b53b3c6424aace4796c363 (patch) | |
| tree | c60cd9484c493cf6984781f6b60409a191cb5bae | |
| parent | 702b4e1cc3e93f26a5215e6018bd744ec25fdb55 (diff) | |
unsafe_type_of -> type_of in ComCoercion.build_id_coercion
| -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).") |