diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index cc4ea5a4a2..82168f9c4a 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -518,7 +518,7 @@ let type_case_branches_with_names env indspec p c = let (params,realargs) = List.chop nparams args in let lbrty = Inductive.build_branches_type ind specif params p in (* Build case type *) - let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in + let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env p (ind,params) then (set_pattern_names env (fst ind) lbrty, conclty) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index fb5927dbf7..15abfefb15 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -112,8 +112,7 @@ let e_type_case_branches env evdref (ind,largs) pj c = let univ = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params p in let n = (snd specif).Declarations.mind_nrealargs in - let ty = - whd_betaiota !evdref (Reduction.betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) in + let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in (lc, ty, univ) let e_judge_of_case env evdref ci pj cj lfj = |