X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fmpresentation.ml;h=09eb6331e085caa2dd1ae94a506ecdd16b4f8beb;hb=ab06d9617b863a42a49f9a407694a9605f500b98;hp=4dde38a366cc88967093b98ae73f7fb51cfeede0;hpb=4a01e6197e070d3eff7a3fe02180597136d81eba;p=helm.git diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml index 4dde38a36..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";;