- let _, _, a, b = B.get e i in
- F.fprintf frm "@[%a@]" (name err) a
- | B.GRef (_, s) ->
- F.fprintf frm "@[$%s@]" (U.string_of_uri s)
- | B.Cast (_, u, t) ->
- F.fprintf frm "@[{%a}.%a@]" (pp_term e) u (pp_term e) t
- | B.Appl (_, v, t) ->
- F.fprintf frm "@[(%a).%a@]" (pp_term e) v (pp_term e) t
- | B.Bind (a, B.Abst (n, w), t) ->
- let f a =
- let ee = B.push e B.empty a (B.abst n w) in
- F.fprintf frm "@[[%a:%a]%a.%a@]" (name C.err) a (pp_term e) w pp_level n (pp_term ee) t
- in
- rename f e a
- | B.Bind (a, B.Abbr v, t) ->
- let f a =
- let ee = B.push e B.empty a (B.abbr v) in
- F.fprintf frm "@[[%a=%a].%a@]" (name C.err) a (pp_term e) v (pp_term ee) t
- in
- rename f e a
- | B.Bind (a, B.Void, t) ->
- let f a =
- let ee = B.push e B.empty a B.Void in
- F.fprintf frm "@[[%a].%a@]" (name C.err) a (pp_term ee) t
- in
- rename f e a
-
-let pp_lenv frm e =
- let pp_entry f e c a b x = f x (*match b with
- | B.Abst (a, w) ->
- let f a = F.fprintf frm "@,@[%a : %a@]" (name C.err) a (pp_term e) w; f a in
- rename f x a
- | B.Abbr (a, v) ->
- let f a = F.fprintf frm "@,@[%a = %a@]" (name C.err) a (pp_term e) v; f a in
- rename f c a
- | B.Void a ->
- let f a = F.fprintf frm "@,%a" (name C.err) a; f a in
- rename f c a
-*) in
+ let _, _, _, y, b = B.get e i in
+ KP.fprintf och "%a" (name err) y
+ | B.GRef (_, s) ->
+ let u = U.string_of_uri s in
+ KP.fprintf och "$%s" (if !G.short then KF.basename u else u)
+ | B.Cast (u, t) ->
+ KP.fprintf och "<%a>.%a" (pp_term st e) u (pp_term st e) t
+ | B.Appl (_, v, t) ->
+ KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t
+ | B.Bind (y, B.Abst (r, n, w), t) ->
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y (B.abst r n w) in
+ KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) y (pp_term st e) w (pp_term st ee) t
+ | B.Bind (y, B.Abbr v, t) ->
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y (B.abbr v) in
+ KP.fprintf och "[%a=%a].%a" (name C.start) y (pp_term st e) v (pp_term st ee) t
+ | B.Bind (y, B.Void, t) ->
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y B.Void in
+ KP.fprintf och "[%a].%a" (name C.start) y (pp_term st ee) t
+
+let pp_lenv st och e =
+ let pp_entry f c a y b x =
+ let y = R.alpha B.mem e y in
+ let x = B.push x c a y b in
+ match b with
+ | B.Abst (_, _, w) ->
+ KP.fprintf och "[%a : %a] " (name C.start) y (pp_term st c) w; f x
+ | B.Abbr v ->
+ KP.fprintf och "[%a = %a] " (name C.start) y (pp_term st c) v; f x
+ | B.Void ->
+ KP.fprintf och "[%a]" (name C.start) y; f x
+ in
+ if e = B.empty then KP.fprintf och "%s" "empty" else