]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/mpresentation.ml
Added method AndInd.
[helm.git] / helm / ocaml / cic_transformations / mpresentation.ml
index 34c65a4174e561f8fd42e9991b4588492f5e1360..3c4f929024b080b311b2abd36898768e3946ec58 100644 (file)
@@ -207,7 +207,7 @@ and print_mrow =
 and print_mtd =
   let module X = Xml in
   function 
-     Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr (print_mpres m)
+     Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr [< (print_mpres m) ; X.xml_nempty ~prefix "mphantom" [] (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >]
 ;;
 
 let print_mpres pres =
@@ -217,7 +217,7 @@ let print_mpres pres =
      [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
       Some "xmlns","helm","http://www.cs.unibo.it/helm" ;
       Some "xmlns","xlink","http://www.w3.org/1999/xlink"
-     ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"] (print_mpres pres))
+     ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None, "rowspacing", "0.6ex"] (print_mpres pres))
  >]