- match c with
- | 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)
+ match strictify c with
+ | `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)