]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/ast2pres.mli
transformations no longer use Content_expression, but rather CicAst
[helm.git] / helm / ocaml / cic_transformations / ast2pres.mli
index 32531a23212644829f8d7dea590e35bb9296e320..20e909869c88028dd49dbdaa5b9fb3fa93afb098 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
-val maxsize : int
+val maxsize: int
+val countterm: int -> CicAst.term -> int
+val is_big: CicAst.term -> bool
 
-val countterm : int -> CicAst.term -> int
+val ast2astBox:
+  ?unicode:bool -> ?priority:int -> ?assoc:bool -> ?tail:string list ->
+  CicAst.term * (Cic.id, string) Hashtbl.t ->
+    CicAst.term Box.box
 
-val pretty_append :
-  (CicAst.term Box.box) list ->
-  CicAst.term ->
-  (CicAst.term Box.box) list ->
-  (CicAst.term Box.box) list
-
-val ast2box:
-  ?priority:int ->
-  ?assoc:bool ->
-  ?attr:CicAst.term_attribute list ->
-  CicAst.term -> CicAst.term Box.box
-
-
-                         
+val ast2mpres:
+  ?priority:int -> ?assoc:bool -> 
+  CicAst.term * (Cic.id, string) Hashtbl.t ->
+    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