X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=ee3e64bd5456d873e0af5f74ca00f2c6213ab5b9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e73e4ec33186a0c420259e31cfc56a3e96cfa1f0;hpb=08ecc780b3b0a4cac7ed72cf68c310e4eeffa2c1;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index e73e4ec33..ee3e64bd5 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -58,19 +58,25 @@ let get_xref = function
   | `Definition d -> d.Con.def_id
   | `Joint jo -> jo.Con.joint_id
 
-let make_row ?(attrs=[]) items concl =
-  match concl with 
-      B.V _ -> (* big! *)
+let hv_attrs =
+  RenderingAttrs.spacing_attributes `BoxML
+  @ RenderingAttrs.indent_attributes `BoxML
+
+let make_row items concl =
+  B.b_hv hv_attrs (items @ [ concl ])
+(*   match concl with 
+      B.V _ -> |+ big! +|
         B.b_v attrs [B.b_h [] items; B.b_indent concl]
-    | _ ->  (* small *)
-	B.b_h attrs (items@[B.b_space; concl])
+    | _ ->  |+ small +|
+        B.b_h attrs (items@[B.b_space; concl]) *)
 
 let make_concl ?(attrs=[]) verb concl =
-  match concl with 
-      B.V _ -> (* big! *)
+  B.b_hv (hv_attrs @ attrs) [ B.b_kw verb; concl ]
+(*   match concl with 
+      B.V _ -> |+ big! +|
         B.b_v attrs [ B.b_kw verb; B.b_indent concl]
-    | _ ->  (* small *)
-	B.b_h attrs [ B.b_kw verb; B.b_space; concl ]
+    | _ ->  |+ small +|
+        B.b_h attrs [ B.b_kw verb; B.b_space; concl ] *)
 
 let make_args_for_apply term2pres args =
  let make_arg_for_apply is_first arg row =