- 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 4dde38a366cc88967093b98ae73f7fb51cfeede0..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";;