new semantics of the -g option completed

[helm.git] / helm / software / helena / src / xml / xmlCrg.ml

diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml
index b04f5f6e15ef7a406a50f17ffbe0d558d76960e3..b2029149be5999b0824ba1511e8f77cfbd44a17c 100644 (file)
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -37,13 +37,13 @@ let lenv_iter map_bind map_appl map_proj st e lenv out tab =
    ignore (aux lenv)
 
 let rec exp_term st e t out tab = match t with
-   | D.TSort (a, l)       ->
+   | D.TSort (a, h)       ->
       let a =
          let err _ = a in
          let f s = {a with E.n_name = Some (s, true)} in
-        H.string_of_sort err f l
+        H.string_of_sort err f h
       in
-      let attrs = [XL.position l; XL.name a] in
+      let attrs = [XL.position h; XL.name a] in
       XL.tag XL.sort attrs out tab
    | D.TLRef (a, i)       ->
       let a = 
@@ -51,11 +51,11 @@ let rec exp_term st e t out tab = match t with
         let f n r = {a with E.n_name = Some (n, r)} in
          D.get_name err f i e
       in
-      let attrs = [XL.position i; XL.name a ] in
+      let attrs = [XL.depth i; XL.name a] in
       XL.tag XL.lref attrs out tab
    | D.TGRef (a, n)       ->
       let a = {a with E.n_name = Some (U.name_of_uri n, true)} in
-      let attrs = [XL.uri n; XL.name a ] in
+      let attrs = [XL.uri n; XL.name a] in
       XL.tag XL.gref attrs out tab
    | D.TCast (a, u, t)    ->
       let attrs = [] in
@@ -81,7 +81,7 @@ and exp_appl st e a x v out tab =
 
 and exp_bind st e a b out tab = match b with
    | D.Abst (_, n, w) ->
-      let attrs = XL.layer st n :: XL.name a :: XL.main a in
+      let attrs = [XL.layer st n; XL.name a] in
       XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
    | D.Abbr v         ->
       let attrs = [XL.name a] in