From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Dec 2006 10:51:43 +0000 (+0000)
Subject: Minor change.
X-Git-Tag: make_still_working~6568
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e850ea466d664062ad1999e75c60b90aadaa084;p=helm.git

Minor change.
---

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([],