]> matita.cs.unibo.it Git - helm.git/blobdiff - components/content_pres/boxPp.mli
map_unicode_to_tex is no longer optional and it always refers to the current
[helm.git] / components / content_pres / boxPp.mli
index 66ae8ec95ea7f15f048bc64abbadb26d9f7f76a2..291c59a2ae1439f3cb22e43efa6f66b71b6a87c0 100644 (file)
@@ -28,7 +28,7 @@
    *  TeX-like macros (when possible). Default: true
    * @return rows list of rows *)
 val render_to_strings: 
-  ?map_unicode_to_tex:bool ->
+  map_unicode_to_tex:bool ->
   (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> 
   int -> CicNotationPres.markup -> string list
 
@@ -37,7 +37,7 @@ val render_to_strings:
    * @return s, concatenation of the return value of render_to_strings above
    * with newlines as separators *)
 val render_to_string:
-  ?map_unicode_to_tex:bool ->
+  map_unicode_to_tex:bool ->
   (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> 
   int -> CicNotationPres.markup -> string