| ESort -> err ()
| EBind (tl, a, _) ->
let err kk = aux f (succ i) (k + kk) tl in
- let f j = f i j k in
+ let f j = f i j (k + j) in
Entity.resolve err f id a
| EProj _ -> assert false (* TODO *)
in
let rec get_name err f i j = function
| ESort -> err i
+ | EBind (tl, a, Abst []) -> get_name err f i j tl
+ | EBind (tl, a, Abbr []) -> get_name err f i j tl
+ | EBind (tl, a, Void 0) -> get_name err f i j tl
| EBind (_, a, _) when i = 0 ->
let err () = err i in
Entity.get_name err f j a