In some cases (e.g. JM equality) the inversion principle is not generated

[helm.git] / helm / software / components / content_pres / termContentPres.ml

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index e925db0aa7085f11e802c23dbbbca2c5bc6d1caa..6b3dcc297689783fbe1a99459cc287764c5d0511 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -75,6 +75,7 @@ let vbox = box Ast.V
 let hvbox = box Ast.HV
 let hovbox = box Ast.HOV
 let break = Ast.Layout Ast.Break
+let space = Ast.Literal (`Symbol " ")
 let builtin_symbol s = Ast.Literal (`Symbol s)
 let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
 
@@ -128,24 +129,26 @@ let pp_ast0 t k =
           match outty_opt with
           | None -> []
           | Some outty ->
-              [ keyword "return"; break; remove_level_info (k outty)]
+              [ space; keyword "return"; space; break; remove_level_info (k outty)]
         in
         let indty_box =
           match indty_opt with
           | None -> []
-          | Some (indty, href) -> [ keyword "in"; break; ident_w_href href indty ]
+          | Some (indty, href) -> [ space; keyword "in"; space; break; ident_w_href href indty ]
         in
         let match_box =
           hvbox false false [
            hvbox false true [
-            hvbox false true [ keyword "match"; break; top_pos (k what) ];
+            hvbox false true [keyword "match"; space; break; top_pos (k what)];
             break;
             hvbox false true indty_box;
             break;
             hvbox false true outty_box
            ];
            break;
-           keyword "with"
+           space;
+           keyword "with";
+           space
          ]
         in
         let mk_case_pattern (head, href, vars) =
@@ -196,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) ->
@@ -216,7 +219,9 @@ let pp_ast0 t k =
           let (params, name, ty, body) = fst_fun in
           hvbox false true ([
             keyword "let";
+            space;
             keyword rec_op;
+            space;
             name] @
             params @
             (match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @