diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c59e085e5..38eea9170 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -53,7 +53,7 @@ let type_constructor mind mib u typ params = let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in - let ndecls = Context.rel_context_length mib.mind_params_ctxt in + let ndecls = Context.Rel.length mib.mind_params_ctxt in if Int.equal ndecls 0 then ctyp else let _,ctyp = decompose_prod_n_assum ndecls ctyp in |