X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=880024ad9386491fd97ca48628b7fe61c7a8b4da;hb=dd627e471392375ca7b6dad78a931a8682e06dbe;hp=23e5a1b56cb68e08c1cd52fa3e10e5e9cefe1368;hpb=db63f65c35efaa93d0a2cc00a194549e791975c9;p=helm.git

diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml
index 23e5a1b56..880024ad9 100644
--- a/matita/components/content_pres/content2pres.ml
+++ b/matita/components/content_pres/content2pres.ml
@@ -1051,13 +1051,14 @@ let nconjlist2pres0 term2pres context =
           Con.dec_id = dec_id ;
           Con.dec_type = ty } = d in
       let r = 
-        Box.b_h [Some "helm", "xref", dec_id] 
-          [ Box.b_object (p_mi []
-            (match dec_name with
-               None -> "_"
-             | Some n -> n)) ;
-            Box.b_space; Box.b_text [] ":"; Box.b_space;
-            term2pres ty] in
+        Box.b_hv [Some "helm", "xref", dec_id] 
+          [ Box.b_h []
+            [ Box.b_object (p_mi []
+               (match dec_name with
+                  None -> "_"
+               | Some n -> n)) ;
+              Box.b_space; Box.b_text [] ":"; ];
+	      Box.indent (term2pres ty)] in
       aux (r::accum) tl
   | (Some (`Definition d))::tl ->
       let