]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/xml/xmlLibrary.ml
- helena: the improved attribute system allows to export the sorts of Pi's
[helm.git] / helm / software / helena / src / xml / xmlLibrary.ml
index 1112f43240a62da00bdfc754fe5e0165ac2d7069..4caa7c1c2f50008b12db6f7ad7ed6d3185cb7503 100644 (file)
@@ -26,10 +26,6 @@ let ext = ".xml"
 
 let obj_root = "ENTITY"
 
-let ccs_name = "ccs.ldc"
-
-let ccs_root = "CCS"
-
 let home = "http://lambdadelta.info/"
 
 let system = F.concat (F.concat home base) "ld.dtd"
@@ -101,15 +97,13 @@ let name a =
    E.name err f a
 
 let apix a =
-   let err () = "age", "" in
-   let f i = "age", string_of_int i in
-   E.apix err f a
+   "position", string_of_int a.E.n_apix
 
 let level st n =
    "level", N.to_string st n
 
-let degr a =
-   "degr", string_of_int a.E.n_degr
+let kind a =
+   "position", string_of_int a.E.n_sort
 
 let meta a =
    let map = function