| `Delift ctx ->
let len_ctx = List.length ctx in
let irl = mk_irl 1 (List.length ctx) in
let lc = List.length source - len_ctx, NCic.Ctx irl in
let u, d, metasenv, subst, o = status#obj in
pp(lazy("delifting as " ^
| `Delift ctx ->
let len_ctx = List.length ctx in
let irl = mk_irl 1 (List.length ctx) in
let lc = List.length source - len_ctx, NCic.Ctx irl in
let u, d, metasenv, subst, o = status#obj in
pp(lazy("delifting as " ^