]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/content_pres/termContentPres.ml
Pretty printing of patterns done almost correctly.
[helm.git] / matita / components / content_pres / termContentPres.ml
index 6846c30b5b9e608fe96af08fbb60b740ccf24b19..12fbb07e17b4010b95d16bb809e33220fb60d82c 100644 (file)
@@ -143,7 +143,7 @@ let pp_ast0 status t k =
         in
         let match_box =
           hvbox false false [
-           hvbox false true [
+           hvbox false false [
             hvbox false true [keyword "match"; space; break; top_pos (k what)];
             break;
             hvbox false true indty_box;
@@ -210,8 +210,8 @@ let pp_ast0 status t k =
               keyword "let"; space;
               hvbox false true [
                 aux_var var; space;
-                builtin_symbol "\\def"; break; top_pos (k s) ];
-              break; space; keyword "in"; space ];
+                builtin_symbol "\\def"; break; top_pos (k s); space; keyword "in"; space ];
+              ];
             break;
             k t ])
     | Ast.LetRec (rec_kind, funs, where) ->