- better handling of proof expansion/contraction

[helm.git] / helm / ocaml / cic_transformations / mpresentation.ml

diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml
index de1172d2a9494c78f8af7085e1342414f770ee6e..09eb6331e085caa2dd1ae94a506ecdd16b4f8beb 100644 (file)
--- 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)
  >]
-;;
+
+