diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 10 |
2 files changed, 9 insertions, 3 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 01b1bc824f..49034b1b1f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -202,7 +202,7 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl = let (mib,mip) = Inductive.lookup_mind_specif tenv indsp in let get_consnarg j = let typi = mis_nf_constructor_type (indsp,mib,mip) (j+1) in - let _,t = decompose_prod_n_assum mip.mind_nparams typi in + let _,t = decompose_prod_n_assum (List.length mip.mind_params_ctxt) typi in List.rev (fst (decompose_prod_assum t)) in let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in let consnargsl = Array.map List.length consnargs in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index adc5932f18..792fe6d2d9 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -150,10 +150,16 @@ let get_constructors env (ind,params) = Array.init (Array.length mip.mind_consnames) (fun j -> get_constructor (ind,mib,mip,params) (j+1)) +let rec instantiate args c = match kind_of_term c, args with + | Prod (_,_,c), a::args -> instantiate args (subst1 a c) + | LetIn (_,b,_,c), args -> instantiate args (subst1 b c) + | _, [] -> c + | _ -> anomaly "too short arity" + let get_arity env (ind,params) = let (mib,mip) = Inductive.lookup_mind_specif env ind in - let arity = body_of_type mip.mind_nf_arity in - destArity (prod_applist arity params) + let arity = mip.mind_nf_arity in + destArity (instantiate params arity) (* Functions to build standard types related to inductive *) let build_dependent_constructor cs = |