Minor change.

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

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index a15200b16a14aea39ea6bc2d991fa94ca2ff2615..7c0ad99c476072685ce7454832f03da6dccfcb50 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -387,7 +387,7 @@ and proof2pres term2pres p =
        match args with
          | [] -> []
          | (Con.ArgProof p)::(Con.Term t)::tl -> 
-             B.H([],([B.b_kw "=";B.b_space;term2pres t;B.b_space]@justification p))::(aux tl)
+             B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw "=";B.b_space;term2pres t;B.b_space]@justification p))::(aux tl)
          | _ -> assert false 
       in
       let hd = 
@@ -395,9 +395,9 @@ and proof2pres term2pres p =
          | Con.Term t -> t 
          | _ -> assert false 
       in
-      B.H([],[term2pres hd; B.b_space; 
+      B.HOV([],[term2pres hd; (* B.b_space; *)
              B.V ([],aux (List.tl conclude.Con.conclude_args))])
-     else if conclude.Con.conclude_method = "Apply" then
+    else if conclude.Con.conclude_method = "Apply" then
       let pres_args = 
         make_args_for_apply term2pres conclude.Con.conclude_args in
       B.H([],