]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/ast2pres.mli
version 0.7.1
[helm.git] / helm / ocaml / cic_transformations / ast2pres.mli
index dc370c2b930c64182d7d148f25eb6fd22b6d8526..5b0e5a7403098a38ccd9064dad47a860ac897e6b 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
-val ast2box:
-  ?priority:int ->
-  ?assoc:bool ->
-  ?attr:CicAst.term_attribute list ->
-  CicAst.term -> CicAst.term Box.box
+val maxsize: int
+val countterm: int -> CicAst.term -> int
+val is_big: CicAst.term -> bool
 
+val ast2astBox:
+  ?unicode:bool -> ?priority:int -> ?assoc:bool -> ?tail:string list ->
+  CicAst.term * (Cic.id, string) Hashtbl.t ->
+    CicAst.term Box.box
 
-                         
+val ast2mpres:
+  ?priority:int -> ?assoc:bool -> 
+  CicAst.term * (Cic.id, string) Hashtbl.t ->
+    unit Mpresentation.mpres
 
+val add_xml_declaration: Xml.token Stream.t -> Xml.token Stream.t
 
+val ast2mpresXml:
+  CicAst.term * (Cic.id, string) Hashtbl.t ->
+    Xml.token Stream.t