X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fxml%2FxmlLibrary.mli;h=552aa36666ee5226c64e2ef5bdc9a7c147f14007;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=19ce4cfe3564357aca2e74695807f847f46e0fdc;hpb=977faf4820cd8ff5e2f0a5249161bbb92ae4b097;p=helm.git

diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli
index 19ce4cfe3..552aa3666 100644
--- a/helm/software/helena/src/xml/xmlLibrary.mli
+++ b/helm/software/helena/src/xml/xmlLibrary.mli
@@ -9,6 +9,8 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+IFDEF OBJECTS THEN
+
 type och = string -> unit
 
 type attr = string * string
@@ -16,9 +18,7 @@ type attr = string * string
 type pp = och -> int -> unit
 
 val export_entity: ('term -> pp) -> 'term Entity.entity -> unit
-(*
-val export_csys: Ccs.csys -> unit
-*)
+
 val tag: string -> attr list -> ?contents:pp -> pp 
 
 val sort: string
@@ -29,7 +29,7 @@ val gref: string
 
 val cast: string
 
-val appl: string
+val appl: bool -> string
 
 val proj: string
 
@@ -41,14 +41,22 @@ val void: string
 
 val position: int -> attr
 
+val depth: int -> attr
+
 val uri: Entity.uri -> attr
 
-val level: Level.level -> attr
+val layer: Layer.status -> Layer.layer -> attr
 
-val name: Entity.node_attrs -> attr
+val name: Entity.bind_attrs -> attr
+
+val main: Entity.bind_attrs -> attr list
+
+val side: Entity.bind_attrs -> attr list
 
 val apix: Entity.node_attrs -> attr
 
 val meta: Entity.root_attrs -> attr
 
 val info: Entity.root_attrs -> attr list
+
+END