From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 21 Jul 2008 11:34:35 +0000 (+0000)
Subject: avoid empty hvbox
X-Git-Tag: make_still_working~4906
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=046ec6faa84164da05d6ec234e68fd2978e70ecf;p=helm.git

avoid empty hvbox
---

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 =