+ | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
+ let ctx =
+ (Some (name,`OfKind Type(*(kind_of status ~metasenv context ty)*)))::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | TSkip t,NCic.Lambda (name, ty, t') ->
+ let ctx = None::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | Top,_ -> assert false (*TODO: HOW??*)