X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fxml%2FxmlCrg.ml;h=b04f5f6e15ef7a406a50f17ffbe0d558d76960e3;hb=2cf2e883f91164ce614bdc86b5c5e2419b98f68d;hp=ec103f7ec93a7961a5d281bbc35e9c50625b6e52;hpb=ac97468f5422efc770316286cb807e3d3245a474;p=helm.git

diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml
index ec103f7ec..b04f5f6e1 100644
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -22,14 +22,14 @@ module D  = Crg
 let lenv_iter map_bind map_appl map_proj st e lenv out tab = 
    let rec aux = function
       | D.ESort           -> e
-      | D.EBind (e, a, b) -> 
+      | 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 st e a b out tab; D.EBind (e, a, b)
-      | D.EAppl (e, a, v) ->
+      | D.EAppl (e, a, x, v) ->
          let e = aux e in
-         map_appl st e a v out tab; D.EAppl (e, a, v)
+         map_appl st e a x v out tab; D.EAppl (e, a, x, v)
       | D.EProj (e, a, d) ->
          let e = aux e in
          map_proj st e a d out tab; D.EProj (e, a, d)
@@ -51,19 +51,19 @@ 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.position 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; XL.apix 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
       XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
       exp_term st e t out tab
-   | D.TAppl (a, v, t)    ->
+   | D.TAppl (a, x, v, t) ->
       let attrs = [] in
-      XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
+      XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
       exp_term st e t out tab
    | D.TProj (a, lenv, t) ->
       let attrs = [] in
@@ -75,18 +75,18 @@ let rec exp_term st e t out tab = match t with
       exp_bind st e a b out tab; 
       exp_term st (D.push_bind C.start a b e) t out tab 
 
-and exp_appl st e a v out tab =
+and exp_appl st e a x v out tab =
    let attrs = [] in
-   XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
+   XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
 
 and exp_bind st e a b out tab = match b with
-   | D.Abst (n, w) ->
-      let attrs = [XL.level st n; XL.name a] in
+   | D.Abst (_, n, w) ->
+      let attrs = XL.layer st n :: XL.name a :: XL.main a in
       XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
-   | D.Abbr v      ->
+   | D.Abbr v         ->
       let attrs = [XL.name a] in
       XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
-   | D.Void        ->
+   | D.Void           ->
       let attrs = [XL.name a] in
       XL.tag XL.void attrs out tab