- new attributes system

[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 ce14855e0abd4b21bd68ea20116d255a545f6e9f..2e10553cb25e3f76841387afbf2aeaae6d0afbc0 100644 (file)
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -12,7 +12,7 @@
 module U  = NUri
 module C  = Cps
 module H  = Hierarchy
-module Y  = Entity
+module E  = Entity
 module R  = Alpha
 module XL = XmlLibrary
 module D  = Crg
@@ -24,6 +24,8 @@ let lenv_iter map_bind map_appl map_proj e lenv out tab =
       | D.ESort           -> e
       | D.EBind (e, a, b) -> 
          let e = aux e in
+(* NOTE: the inner binders are alpha-converted first *)
+         let a = R.alpha D.mem e a in
          map_bind e a b out tab; D.EBind (e, a, b)
       | D.EAppl (e, a, v) ->
          let e = aux e in
@@ -38,7 +40,7 @@ let rec exp_term e t out tab = match t with
    | D.TSort (a, l)       ->
       let a =
          let err _ = a in
-         let f s = Y.Name (s, true) :: a in
+         let f s = {a with E.n_name = Some (s, true)} in
         H.string_of_sort err f l
       in
       let attrs = [XL.position l; XL.name a] in
@@ -46,13 +48,13 @@ let rec exp_term e t out tab = match t with
    | D.TLRef (a, i)       ->
       let a = 
          let err _ = a in
-        let f n r = Y.Name (n, r) :: a in
+        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
       XL.tag XL.lref attrs out tab
    | D.TGRef (a, n)       ->
-      let a = Y.Name (U.name_of_uri n, true) :: a in
+      let a = {a with E.n_name = Some (U.name_of_uri n, true)} in
       let attrs = [XL.uri n; XL.name a; XL.apix a] in
       XL.tag XL.gref attrs out tab
    | D.TCast (a, u, t)    ->
@@ -69,7 +71,7 @@ let rec exp_term e t out tab = match t with
       exp_term (D.push_proj C.start a lenv e) t out tab
    | D.TBind (a, b, t) ->
 (* NOTE: the inner binders are alpha-converted first *)
-      let a = R.alpha (D.names_of_lenv [] e) a in
+      let a = R.alpha D.mem e a in
       exp_bind e a b out tab; 
       exp_term (D.push_bind C.start a b e) t out tab 
 
@@ -79,7 +81,7 @@ and exp_appl e a v out tab =
 
 and exp_bind e a b out tab = match b with
    | D.Abst (n, w) ->
-      let attrs = [XL.level n; XL.name a; XL.mark a] in
+      let attrs = [XL.level n; XL.name a] in
       XL.tag XL.abst attrs ~contents:(exp_term e w) out tab
    | D.Abbr v      ->
       let attrs = [XL.name a] in