- | NCic.Appl l -> List.fold_left f acc l
- | NCic.Prod (_,s,t)
- | NCic.Lambda (_,s,t) -> f (g (f acc s)) t
- | NCic.LetIn (_,ty,t,bo) -> f (g (f (f acc ty) t)) bo
- | NCic.Match (_,oty,t,pl) -> List.fold_left f (f (f acc oty) t) pl
+ | NCic.Appl [] | NCic.Appl [_] -> assert false
+ | NCic.Appl l -> List.fold_left (f k) acc l
+ | NCic.Prod (n,s,t)
+ | NCic.Lambda (n,s,t) -> f (g (n,NCic.Decl s) k) (f k acc s) t
+ | NCic.LetIn (n,ty,t,bo) -> f (g (n,NCic.Def (t,ty)) k) (f k (f k acc ty) t) bo
+ | NCic.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl