diff options
| author | Maxime Dénès | 2018-02-12 13:07:53 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-12 13:07:53 +0100 |
| commit | 284869d016607fad339ea4d06bf1433c6ec23672 (patch) | |
| tree | 1cae1f278186bb0aa9643fb57ca9af0eb029672f /pretyping | |
| parent | 52d666a7a83e4023d9f5cd7324ed81c7f7926156 (diff) | |
| parent | 42610a4659cf35e6a005d79eec273c606bdf87dd (diff) | |
Merge PR #1082: Fixing Print for inductive types with let-in in parameters
Diffstat (limited to 'pretyping')
| -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 b21fbf0eb2..c93b41786b 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -240,8 +240,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 *) |