]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/complete_rg/crgOutput.ml
last commit for helena 0.8.2
[helm.git] / helm / software / helena / src / complete_rg / crgOutput.ml
index 7275dd462c604618e6d4242fb6b182134d0a44a7..7c9ab81724ec0befa9d37f77bf44ab07cc5a4ce1 100644 (file)
@@ -145,12 +145,12 @@ let rec pp_term out st = function
 
 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 "} "