diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-14 15:18:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:00 +0200 |
| commit | 3869ffab2021b076054280f5eb4226ecda8caf75 (patch) | |
| tree | af6cae718a2b6e4acf72794cbe6677d253ede62f /pretyping/pretyping.ml | |
| parent | d2f36624980cdc169d0ebcc4c0be66446b4a8936 (diff) | |
- Add back some compatibility functions to avoid rewriting plugins.
- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 18b96e765..8e65cc480 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -507,7 +507,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = if Int.equal npars 0 then [] else try - let ty = evd_comb1 (Coercion.inh_coerce_to_prod loc env) evdref ty in let IndType (indf, args) = find_rectype env !evdref ty in let ((ind',u'),pars) = dest_ind_family indf in if eq_ind ind ind' then pars |