From 2cc1435cba8bd6c7cefd9e34d22080574a8a6890 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 12 Jan 2012 12:03:29 +0000 Subject: [PATCH] Improves the presentation of hypotheses in the goal pane. --- matita/components/content_pres/content2pres.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) 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 -- 2.39.2