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 e5d73b6e2a..343fae48a3 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -344,7 +344,7 @@ let build_branches_type ind (_,mip as specif) params p = (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) let build_case_type n p c realargs = - betazeta_appvect (n+1) p (Array.of_list (realargs@[c])) + whd_betaiota (betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) let type_case_branches env (ind,largs) pj c = let specif = lookup_mind_specif env ind in |