diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 083661a64b..ff528bd2cf 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -61,7 +61,8 @@ let find_rectype_a env c = (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib u typ params = +let type_constructor mind mib u (ctx, typ) params = + let typ = it_mkProd_or_LetIn typ ctx in let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in |