X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fmpresentation.ml;h=09eb6331e085caa2dd1ae94a506ecdd16b4f8beb;hb=ab06d9617b863a42a49f9a407694a9605f500b98;hp=de1172d2a9494c78f8af7085e1342414f770ee6e;hpb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;p=helm.git

diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml
index de1172d2a..09eb6331e 100644
--- a/helm/ocaml/cic_transformations/mpresentation.ml
+++ b/helm/ocaml/cic_transformations/mpresentation.ml
@@ -92,20 +92,20 @@ let two_rows_table_with_brackets attr a b op =
   (* only the open bracket is added; the closed bracket must be in b *)
   Mtable(attr@standard_tbl_attr,
     [Mtr([],[Mtd([],Mrow([],[Mtext([],"(");a]))]);
-     Mtr([],[Mtd([],Mrow([],[indentation;op;smallskip;b]))])]);;
+     Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);;
 
 let two_rows_table_without_brackets attr a b op =
   Mtable(attr@standard_tbl_attr,
     [Mtr([],[Mtd([],a)]);
-     Mtr([],[Mtd([],Mrow([],[indentation;op;smallskip;b]))])]);;
+     Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);;
 
 let row_with_brackets attr a b op =
   (* by analogy with two_rows_table_with_brackets we only add the
      open brackets *)
-  Mrow(attr,[Mtext([],"(");a;smallskip;op;smallskip;b])
+  Mrow(attr,[Mtext([],"(");a;op;b])
 
 let row_without_brackets attr a b op =
-  Mrow(attr,[a;smallskip;op;smallskip;b])
+  Mrow(attr,[a;op;b])
 
 (* MathML prefix *)
 let prefix = "m";;
@@ -219,4 +219,5 @@ let print_mpres pres =
       Some "xmlns","xlink","http://www.w3.org/1999/xlink"
      ] (print_mpres pres)
  >]
-;;
+
+