From 5f94d6c85429545d90acc39a9b9fc9a2da33d567 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 20 Jan 2007 15:31:18 +0000 Subject: [PATCH] Bug fixed: if the context of a sequent was empty a vertical box without content was generated. This is not allowed by BoxPp (assert failure). --- helm/software/components/content_pres/sequent2pres.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml index 88c804b7d..391b178a2 100644 --- a/helm/software/components/content_pres/sequent2pres.ml +++ b/helm/software/components/content_pres/sequent2pres.ml @@ -83,16 +83,17 @@ let sequent2pres term2pres (_,_,context,ty) = aux (r::accum) tl | _::_ -> assert false in aux [] context in - let pres_context = (Box.b_v [] (context2pres context)) in + let pres_context = + if context <> [] then [Box.b_v [] (context2pres context)] else [] in let pres_goal = term2pres ty in (Box.b_h [] [ Box.b_space; (Box.b_v [] - [Box.b_space; - pres_context; + (Box.b_space :: + pres_context @ [ b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *) Box.b_space; - pres_goal])]) + pres_goal]))]) let sequent2pres ~ids_to_inner_sorts = sequent2pres -- 2.39.2