- | B.Cast (_, u, t) ->
- F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
- | B.Appl (_, v, t) ->
- F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
- | B.Bind (B.Abst (a, w), t) ->
- let f a cc =
- F.fprintf frm "@[[%a:%a].%a@]" name a (pp_term c) w (pp_term cc) t
+ | 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 w, t) ->
+ let f a =
+ let ee = B.push e B.empty a (B.abst w) in
+ F.fprintf frm "@[[%a:%a].%a@]" (name C.err) a (pp_term e) w (pp_term ee) t