From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 12 Jan 2012 12:03:29 +0000 (+0000)
Subject: Improves the presentation of hypotheses in the goal pane.
X-Git-Tag: make_still_working~1979
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2cc1435cba8bd6c7cefd9e34d22080574a8a6890;p=helm.git

Improves the presentation of hypotheses in the goal pane.
---

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