diff options
| author | Pierre-Marie Pédrot | 2015-02-28 00:58:29 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-28 00:58:29 +0100 |
| commit | fcd7926fa8bddc86f66e936ad0bf615326b8cb6d (patch) | |
| tree | fb1be444a7b66b253e27c93b23eb229aacee0645 /kernel | |
| parent | 2206b405c19940ca4ded2179d371c21fd13f1b6b (diff) | |
| parent | 78d1a61730886f89b01fa4245e58b54dd50fb4cf (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'kernel')
| -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 6b4dd536a1..ca814f497c 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -364,7 +364,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@(local_rels args)) in vargs @ [dep_cstr] in - let base = beta_appvect (lift nargs p) (Array.of_list cargs) in + let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base args in Array.mapi build_one_branch mip.mind_nf_lc |