diff options
Diffstat (limited to 'plugins/subtac/subtac_coercion.ml')
| -rw-r--r-- | plugins/subtac/subtac_coercion.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 1bc3dbb345..3c907962ce 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -456,8 +456,8 @@ module Coercion = struct let (evd', val') = try inh_conv_coerce_to_fail loc env evd rigidonly - (Some (nf_isevar evd cj.uj_val)) - (nf_isevar evd cj.uj_type) (nf_isevar evd t) + (Some (nf_evar evd cj.uj_val)) + (nf_evar evd cj.uj_type) (nf_evar evd t) with NoCoercion -> let sigma = evd in try |