- | B.Bind (a, B.Abst (r, n, w), t) ->
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abst r n w) in
- KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) a (pp_term st e) w (pp_term st ee) t
- | B.Bind (a, B.Abbr v, t) ->
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abbr v) in
- KP.fprintf och "[%a=%a].%a" (name C.start) a (pp_term st e) v (pp_term st ee) t
- | B.Bind (a, B.Void, t) ->
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a B.Void in
- KP.fprintf och "[%a].%a" (name C.start) a (pp_term st ee) 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