]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/xml/xmlLibrary.ml
- bug fix in the static analyzer allows better Pi/forall separation (exportation...
[helm.git] / helm / software / helena / src / xml / xmlLibrary.ml
index 3c77fe68bc3edb36620323035601e17ef76725a1..dcc18c94b125a49c92928190820b68c278cc2b23 100644 (file)
@@ -96,14 +96,23 @@ let name a =
    let f n r = "name", if r then n else "-" ^ n in 
    E.name err f a
 
-let apix a =
-   "position", string_of_int a.E.n_apix
-
 let layer st n =
    "layer", N.to_string st n
 
-let kind a =
-   "position", string_of_int a.E.n_sort
+let main a =
+   let sort, degr = a.E.n_main in
+   ["main-sort", string_of_int sort;
+    "main-degree", string_of_int degr;
+   ]
+
+let side a =
+   let sort, degr = a.E.n_side in
+   ["side-sort", string_of_int sort;
+    "side-degree", string_of_int degr;
+   ]
+
+let apix a =
+   "level", string_of_int a.E.n_apix
 
 let meta a =
    let map = function