- let pp_entry f e c a b x = f x (* match b with
- | B.Abst (a, w) ->
- let a = R.alpha B.mem e a in
- KP.fprintf och "%a : %a\n" (name C.start) a (pp_term st e) w; f a
- | B.Abbr (a, v) ->
- let a = R.alpha B.mem e a in
- KP.fprintf och "%a = %a\n" (name C.start) a (pp_term st e) v; f a
- | B.Void a ->
- let a = R.alpha B.mem e a in
- KP.fprintf och "%a\n" (name C.start) a; f a
-*) in
- let e = B.empty in
- if e = B.empty then KP.fprintf och "%s\n" "not shown" else
+ let pp_entry f c a b x =
+ let a = R.alpha B.mem e a in
+ let x = B.push x c a b in
+ match b with
+ | B.Abst (_, _, w) ->
+ KP.fprintf och "[%a : %a] " (name C.start) a (pp_term st c) w; f x
+ | B.Abbr v ->
+ KP.fprintf och "[%a = %a] " (name C.start) a (pp_term st c) v; f x
+ | B.Void ->
+ KP.fprintf och "[%a]" (name C.start) a; f x
+ in
+ if e = B.empty then KP.fprintf och "%s" "empty" else