implemented transformations on top of notation code

[helm.git] / helm / ocaml / cic_notation / cicNotationPres.mli

diff --git a/helm/ocaml/cic_notation/cicNotationPres.mli b/helm/ocaml/cic_notation/cicNotationPres.mli
index 68da94458dfd3fb630739811cfb23a18448bc322..f507dc6bf44e35a1110490f9452a297dd83178a8 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPres.mli
+++ b/helm/ocaml/cic_notation/cicNotationPres.mli
@@ -32,9 +32,16 @@ type markup = mathml_markup
  * @param ids_to_uris mapping id -> uri for hyperlinking *)
 val render: (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> markup
 
+(** @param ids_to_uris *)
 val render_to_boxml:
   (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> Xml.token Stream.t
 
 (* val render_to_mathml:
   (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> mathml_markup *)
 
+val mpres_of_box: boxml_markup -> mathml_markup
+val box_of_mpres: mathml_markup -> boxml_markup
+
+val print_mpres:  mathml_markup -> Xml.token Stream.t
+val print_box:    boxml_markup -> Xml.token Stream.t
+