diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 09:51:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 09:51:42 +0100 |
| commit | ff8d99117f142dd6851eb7cecc0ae84ec8642fe1 (patch) | |
| tree | d739c888812b934ee7866e07a299ffcc8456ef11 /kernel/inductive.ml | |
| parent | e3e86829780f664ae7a81582a4c6251ceec4f622 (diff) | |
Contracting one extra beta-redex on the fly when typing branches of "match".
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 |