]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/xml/xmlLibrary.mli
when sort inclusion is enabled, we can produce conversion constraints in xml
[helm.git] / helm / software / lambda-delta / src / xml / xmlLibrary.mli
index 28f056f068a6a01f8cacf2e9a8f4584b17768c04..ebd4157d9f0d0567134b4210b975be3c64306f37 100644 (file)
@@ -15,8 +15,9 @@ type attr = string * string
 
 type pp = och -> int -> unit
 
-val export_entity:
-   ('term -> pp) -> bool -> string -> 'term Entity.entity -> unit
+val export_entity: ('term -> pp) -> 'term Entity.entity -> unit
+
+val export_csys: Ccs.csys -> unit
 
 val tag: string -> attr list -> ?contents:pp -> pp 
 
@@ -44,7 +45,7 @@ val offset: int -> attr
 
 val uri: Entity.uri -> attr
 
-val arity: int -> attr
+val arity: ?n:int -> 'a list -> attr
 
 val level: Level.level -> attr