diff options
| author | Pierre-Marie Pédrot | 2016-11-26 02:12:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:43 +0100 |
| commit | c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 (patch) | |
| tree | f57eaac2d0c3cee82b172556eca53f16e0f0a900 /pretyping/coercion.ml | |
| parent | 01849481fbabc3a3fa6c483e703996b01e37fca5 (diff) | |
Evar-normalizing functions now act on EConstrs.
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 ead44cee2f..91f53a886d 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 -> |