X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fsequent2pres.ml;h=d9c3a325e808a7d531dddd37d2a9be124ff1a967;hb=ce98548577a44fafd17f1d9ce42bca1e6db104fc;hp=391b178a27c3036fbfa450e1ea9240b7d2ff9968;hpb=5f94d6c85429545d90acc39a9b9fc9a2da33d567;p=helm.git

diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml
index 391b178a2..d9c3a325e 100644
--- a/helm/software/components/content_pres/sequent2pres.ml
+++ b/helm/software/components/content_pres/sequent2pres.ml
@@ -64,7 +64,7 @@ let sequent2pres term2pres (_,_,context,ty) =
                (match dec_name with
                   None -> "_"
                 | Some n -> n)) ;
-               Box.b_text [] ":" ;
+               Box.b_space; Box.b_text [] ":"; Box.b_space;
                term2pres ty] in
          aux (r::accum) tl
      | (Some (`Definition d))::tl ->
@@ -77,9 +77,9 @@ let sequent2pres term2pres (_,_,context,ty) =
               [ Box.b_object (p_mi []
                 (match def_name with
                    None -> "_"
-                 | Some n -> n)) ;
-                 Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
-                term2pres bo] in
+                 | Some n -> n)) ; Box.b_space ;
+                Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
+                Box.b_space; term2pres bo] in
          aux (r::accum) tl
       | _::_ -> assert false in
       aux [] context in
@@ -99,7 +99,7 @@ let sequent2pres ~ids_to_inner_sorts =
   sequent2pres
     (fun annterm ->
       let ast, ids_to_uris =
-        TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
+       TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
       in
       CicNotationPres.box_of_mpres
         (CicNotationPres.render ids_to_uris