diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 214aac5ec0..2defb66f4b 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -630,9 +630,12 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = (* Type of constructors in normal form *) let splayed_lc = Array.map (dest_prod_assum env_ar) lc in let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in - let consnrealargs = + let consnrealdecls = Array.map (fun (d,_) -> rel_context_length d - rel_context_length params) splayed_lc in + let consnrealargs = + Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params) + splayed_lc in (* Elimination sorts *) let arkind,kelim = match ar_kind with | Inr (param_levels,lev) -> @@ -668,7 +671,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls; mind_kelim = kelim; mind_consnames = Array.of_list cnames; - mind_consnrealdecls = consnrealargs; + mind_consnrealdecls = consnrealdecls; + mind_consnrealargs = consnrealargs; mind_user_lc = lc; mind_nf_lc = nf_lc; mind_recargs = recarg; |