X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;fp=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=fc3a47b5e1c564fb168e1fcba94b09ccd40fa86e;hb=c699a9669505947487dce49383fa50fe9b9968e8;hp=8fe5657b32feeb2cba52a68d8d704199f54d202e;hpb=b637879a2b3f2ceda65afb3c950061189c4730b7;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 8fe5657b3..fc3a47b5e 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -835,7 +835,7 @@ let conjecture2pres term2pres (id, n, context, ty) =
 			    (match dec_name with
 				 None -> "_"
 			       | Some n -> n));
-                       B.b_text [] ":";
+                       B.b_text [] ":"; B.b_space; 
                        term2pres ty ]
              | Some (`Definition d) ->
                  let
@@ -848,6 +848,7 @@ let conjecture2pres term2pres (id, n, context, ty) =
 					  None -> "_"
 					| Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
+                       B.b_space;
                        term2pres bo]
              | Some (`Proof p) ->
                  let proof_name = p.Content.proof_name in
@@ -857,12 +858,16 @@ let conjecture2pres term2pres (id, n, context, ty) =
 					  None -> "_"
 					| Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
+                       B.b_space;
                        proof2pres true term2pres p])
           (List.rev context)))) ] ::
          [ B.b_h []
-           [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
+           [ B.b_space; 
+             B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
+             B.b_space;
              B.b_object (p_mi [] (string_of_int n)) ;
              B.b_text [] ":" ;
+             B.b_space;
              term2pres ty ]])))
 
 let metasenv2pres term2pres = function