avoid empty hvbox

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 013e3a872fabcff73824e786fcae9982b52c2a4a..3ee9e7fe9f90d266d4ba4e158684e0bda3a50634 100644 (file)
--- 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 =