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 /pretyping/inductiveops.ml | |
| parent | 2206b405c19940ca4ded2179d371c21fd13f1b6b (diff) | |
| parent | 78d1a61730886f89b01fa4245e58b54dd50fb4cf (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index adf714db35..7f6a4a6442 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -273,7 +273,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in let ind_tags = - rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in + rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in let cstr_tags = Array.map2 (fun c n -> let d,_ = decompose_prod_assum c in @@ -526,7 +526,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.beta_appvect p (Array.of_list (realargs@[c])) in + let conclty = Reduction.betazeta_appvect (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) |