]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/xml/xmlLibrary.ml
new semantics of the -g option completed
[helm.git] / helm / software / helena / src / xml / xmlLibrary.ml
index dcc18c94b125a49c92928190820b68c278cc2b23..002688b31dae912534ae0818eb7b75dae5a8f6d7 100644 (file)
@@ -88,6 +88,9 @@ let void = "Void"
 let position i =
    "position", string_of_int i
 
+let depth i =
+   "depth", string_of_int i
+
 let uri u =
    "uri", U.string_of_uri u
 
@@ -101,13 +104,13 @@ let layer st n =
 
 let main a =
    let sort, degr = a.E.n_main in
-   ["main-sort", string_of_int sort;
+   ["main-position", 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-position", string_of_int sort;
     "side-degree", string_of_int degr;
    ]