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

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