From 42610a4659cf35e6a005d79eec273c606bdf87dd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 23 Sep 2017 12:46:35 +0200 Subject: Vm_compute: taking into account let-ins in parameters of constructors. --- pretyping/vnorm.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping/vnorm.ml') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b5b8987e3..9cc635ed1 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -239,8 +239,9 @@ and nf_stk ?from:(from=0) env sigma c t stk = let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in + hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) -- cgit v1.2.3