From ff8d99117f142dd6851eb7cecc0ae84ec8642fe1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 5 Dec 2015 09:51:42 +0100 Subject: Contracting one extra beta-redex on the fly when typing branches of "match". --- kernel/inductive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/inductive.ml') 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 -- cgit v1.2.3