diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index e06ea75e6..cefb5eca5 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -365,7 +365,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let cstr = ith_constructor_of_inductive ind (i+1) in let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in vargs @ [dep_cstr] in - let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in + let base = betazeta_appvect (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base cstrsign in Array.mapi build_one_branch mip.mind_nf_lc |