From 046ec6faa84164da05d6ec234e68fd2978e70ecf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 21 Jul 2008 11:34:35 +0000 Subject: [PATCH] avoid empty hvbox --- helm/software/components/content_pres/termContentPres.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 013e3a872..3ee9e7fe9 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -359,7 +359,8 @@ let instantiate21 idrefs env l1 = let terms = subst pos env p in instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl in - [hovbox false false (instantiate_list [] values)] + if values = [] then [] + else [hovbox false false (instantiate_list [] values)] | Ast.Opt p -> let opt_decls = CicNotationEnv.declarations_of_term p in let env = -- 2.39.2