diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index c7110d7a91..e77c5082dd 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -614,7 +614,7 @@ let is_elim_predicate_explicitly_dependent env sigma pred indf = let set_names env sigma n brty = let open EConstr in let (ctxt,cl) = decompose_prod_n_assum sigma n brty in - EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt) + Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt let set_pattern_names env sigma ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -631,11 +631,12 @@ let type_case_branches_with_names env sigma indspec p c = let nparams = mib.mind_nparams in let (params,realargs) = List.chop nparams args in let lbrty = Inductive.build_branches_type ind specif params p in + let lbrty = Array.map EConstr.of_constr lbrty in (* Build case type *) 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 sigma p (ind,params) then - (set_pattern_names env sigma (fst ind) (Array.map EConstr.of_constr lbrty), conclty) + (set_pattern_names env sigma (fst ind) lbrty, conclty) else (lbrty, conclty) (* Type of Case predicates *) |