diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e5023e858..fe9646b9d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -532,8 +532,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = (mk_tycon (applist (mkIndU ind, args))) in j', (ind, args)) in - let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in - let ty = Vars.subst_univs_level_constr usubst ty in + let ty = Vars.subst_instance_constr u ty in let ty = substl (recty.uj_val :: List.rev pars) ty in let j = {uj_val = mkProj (cst,recty.uj_val); uj_type = ty} in inh_conv_coerce_to_tycon loc env evdref j tycon |