From 3b3a14912c135dc45da970d71235b630660d88c8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 16 Jul 2008 16:16:30 +0000
Subject: [PATCH] notations for lists adds some breaking points

---
 helm/software/components/content_pres/termContentPres.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index fd326e5e9..013e3a872 100644
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -346,7 +346,7 @@ let instantiate21 idrefs env l1 =
         let sep =
           match sep_opt with
             | None -> []
-            | Some l -> [ Ast.Literal l ]
+            | Some l -> [ Ast.Literal l; break; space ]
 	in
         let rec instantiate_list acc = function
           | [] -> List.rev acc
@@ -359,7 +359,7 @@ let instantiate21 idrefs env l1 =
               let terms = subst pos env p in
               instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
         in
-        instantiate_list [] values
+        [hovbox false false (instantiate_list [] values)]
     | Ast.Opt p ->
         let opt_decls = CicNotationEnv.declarations_of_term p in
         let env =
-- 
2.39.2