diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b21f4e383..758686aa9 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -58,8 +58,7 @@ let find_rectype_a env c = let type_constructor mind mib u typ params = let s = ind_subst mind mib u in let ctyp = substl s typ in - let usubst = make_inductive_subst mib u in - let ctyp = subst_univs_level_constr usubst ctyp in + let ctyp = subst_instance_constr u ctyp in let nparams = Array.length params in if Int.equal nparams 0 then ctyp else |