- | C.Prod (n,s,t) -> aux ctx s ; aux (((*P.Declaration,*)n,s)::ctx) t
- | C.Lambda (n,s,t) -> aux ctx s ; aux (((*P.Declaration,*)n,s)::ctx) t
- | C.LetIn (n,s,t) ->
- aux ctx s ; assert false (* aux ([P.Definition,n,s]::ctx) t *)
+ | C.Prod (n,s,t) -> aux ctx s ; aux ((n, C.Decl s)::ctx) t
+ | C.Lambda (n,s,t) -> aux ctx s ; aux ((n, C.Decl s)::ctx) t
+ | C.LetIn (n,s,t) -> aux ctx s ; aux ((n, C.Def s)::ctx) t