- | Ce (name, NCic.Def (bo,ty)) -> NCic.LetIn (name, ty, bo, t)
- | Ce (name, NCic.Decl ty) when mk_pi -> NCic.Prod (name, ty, t)
- | Ce (name, NCic.Decl ty) -> NCic.Lambda (name, ty, t)
- | Fix (_,name,ty) when mk_pi -> NCic.Prod (name, ty, t)
- | Fix (_,name,ty) -> NCic.Lambda (name,ty,t))
- t ctx
+ | Ce ((name, NCic.Def (bo,ty)),l') -> NCic.LetIn (name, ty, bo, t),l@l'
+ | Ce ((name, NCic.Decl ty),l') when mk_pi -> NCic.Prod (name, ty, t),l@l'
+ | Ce ((name, NCic.Decl ty),l') -> NCic.Lambda (name, ty, t),l@l'
+ | Fix (_,name,ty) when mk_pi -> NCic.Prod (name, ty, t),l
+ | Fix (_,name,ty) -> NCic.Lambda (name,ty,t),l)
+ (t,[]) ctx