]> matita.cs.unibo.it Git - helm.git/commitdiff
avoid empty hvbox
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 21 Jul 2008 11:34:35 +0000 (11:34 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 21 Jul 2008 11:34:35 +0000 (11:34 +0000)
helm/software/components/content_pres/termContentPres.ml

index 013e3a872fabcff73824e786fcae9982b52c2a4a..3ee9e7fe9f90d266d4ba4e158684e0bda3a50634 100644 (file)
@@ -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 =