diff options
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index ead44cee2..91f53a886 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -417,7 +417,6 @@ let inh_tosort_force loc env evd j = try let t,p = lookup_path_to_sort_from env evd j.uj_type in let evd,j1 = apply_coercion env evd p j t in - let whd_evar evd c = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr c)) in let j2 = on_judgment_type (whd_evar evd) j1 in (evd,type_judgment env evd j2) with Not_found | NoCoercion -> |