X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2Fcontent2pres.ml;h=7c0ad99c476072685ce7454832f03da6dccfcb50;hb=c651530ffbff86d63868f452ec4fdc59488fc4ee;hp=a15200b16a14aea39ea6bc2d991fa94ca2ff2615;hpb=57f678d84d02772bfe36301d2f367c2382583f16;p=helm.git

diff --git a/components/content_pres/content2pres.ml b/components/content_pres/content2pres.ml
index a15200b16..7c0ad99c4 100644
--- a/components/content_pres/content2pres.ml
+++ b/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([],