and pp_bind out st = function
| D.Abst (n, x) ->
- out "[:"; pp_term out st x; out "]"; out (N.to_string st n)
- | D.Abbr x -> out "[="; pp_term out st x; out "]";
- | D.Void -> out "[]"
+ out "[:"; pp_term out st x; out "]"; out (N.to_string st n); out " "
+ | D.Abbr x -> out "[="; pp_term out st x; out "] ";
+ | D.Void -> out "[] "
and pp_lenv out st = function
| D.ESort -> ()
| D.EBind (x, a, y) -> pp_lenv out st x; pp_attrs out a; pp_bind out st y
- | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ")"
- | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "}"
+ | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ") "
+ | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "} "