+ | Top ->
+ let arg =
+ match classify status ~metasenv context arg with
+ | `PropKind
+ | `Proposition
+ | `Term `TypeFormer
+ | `Term `PropFormer
+ | `Term `Proof
+ | `Type
+ | `KindOrType
+ | `Kind -> UnitTerm
+ | `Term `TypeFormerOrTerm
+ | `Term `Term -> term_of status ~metasenv context arg
+ in
+ eat_args status metasenv (UnsafeCoerce (mk_appl acc arg))
+ context Top tl