diff options
| author | Hugo Herbelin | 2017-09-23 12:46:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-12-14 15:57:51 +0100 |
| commit | 42610a4659cf35e6a005d79eec273c606bdf87dd (patch) | |
| tree | 8a3168b468796527f8c95ab358534ff094d78388 | |
| parent | c248228f5e910e19114e827661abb255c77a2b01 (diff) | |
Vm_compute: taking into account let-ins in parameters of constructors.
| -rw-r--r-- | pretyping/vnorm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b5b8987e33..9cc635ed1d 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 *) |