From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 16 Jul 2008 16:16:30 +0000 (+0000)
Subject: notations for lists adds some breaking points
X-Git-Tag: make_still_working~4920
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3b3a14912c135dc45da970d71235b630660d88c8;p=helm.git

notations for lists adds some breaking points
---

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 =