| `Ce ((_, NCic.Def _),_) -> aux (n-1,tl))
| _,_ -> assert false
in
- NCic.Appl (t:: aux (List.length ctx,rels))
+ let args = aux (List.length ctx,rels) in
+ match args with
+ [] -> t
+ | _::_ -> NCic.Appl (t::args)
;;
let splat_args ctx t n_fix rels =