]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/termContentPres.ml
Procedural: some improvements
[helm.git] / helm / software / components / content_pres / termContentPres.ml
index a8bfe114746f5c9d79968d7c96141de6d8f27646..6b3dcc297689783fbe1a99459cc287764c5d0511 100644 (file)
@@ -199,10 +199,10 @@ let pp_ast0 t k =
         add_level_info Ast.let_in_prec Ast.let_in_assoc
           (hvbox false true [
             hvbox false true [
-              keyword "let";
+              keyword "let"; space;
               hvbox false true [
-                aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ];
-              break; keyword "in" ];
+                aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ];
+              break; space; keyword "in" ];
             break;
             k t ])
     | Ast.LetRec (rec_kind, funs, where) ->