X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fxml%2FxmlCrg.ml;h=34c78dd9e0a1b78c591ae832cb2d3feca3b60ecc;hp=5d112bed2d1dcd7ebc924556711f41db9006a439;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hpb=fdb80b08af83b86759833142456ce3c4f84cd80e

diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml
index 5d112bed2..34c78dd9e 100644
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -29,9 +29,9 @@ let lenv_iter map_bind map_appl map_proj st e lenv out tab =
 (* NOTE: the inner binders are alpha-converted first *)
          let y = R.alpha D.mem e y in
          map_bind st e a y b out tab; D.EBind (e, a, y, b)
-      | D.EAppl (e, x, v)    ->
+      | D.EAppl (e, a, v)    ->
          let e = aux e in
-         map_appl st e x v out tab; D.EAppl (e, x, v)
+         map_appl st e a v out tab; D.EAppl (e, a, v)
       | D.EProj (e, d)       ->
          let e = aux e in
          map_proj st e d out tab; D.EProj (e, d)
@@ -63,33 +63,33 @@ let rec exp_term st e t out tab = match t with
       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 (x, v, t) ->
-      let attrs = [] in
-      XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
+   | D.TAppl (a, v, t) ->
+      let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in
+      XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
       exp_term st e t out tab
    | D.TProj (lenv, t) ->
       let attrs = [] in
       XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab;
       exp_term st (D.push_proj C.start lenv e) t out tab
-   | D.TBind (y, b, t) ->
+   | D.TBind (a, b, t) ->
 (* NOTE: the inner binders are alpha-converted first *)
-      let y = R.alpha D.mem e y in
-      exp_bind st e E.empty_node y b out tab; 
-      exp_term st (D.push_bind C.start E.empty_node y b e) t out tab 
+      let a = R.alpha D.mem e a in
+      exp_bind st e E.empty_node a b out tab; 
+      exp_term st (D.push_bind C.start E.empty_node a b e) t out tab 
 
-and exp_appl st e x v out tab =
-   let attrs = [] in
-   XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
+and exp_appl st e a v out tab =
+   let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in
+   XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
 
-and exp_bind st e a y b out tab = match b with
+and exp_bind st e y a b out tab = match b with
    | D.Abst (_, n, w) ->
-      let attrs = XL.layer st n :: XL.name y :: XL.side y @ XL.main y in
+      let attrs = XL.layer st n :: XL.name a :: XL.side a.E.b_side @ XL.main a.E.b_main in
       XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
    | D.Abbr v         ->
-      let attrs = [XL.name y] in
+      let attrs = [XL.name a] in
       XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
    | D.Void           ->
-      let attrs = [XL.name y] in
+      let attrs = [XL.name a] in
       XL.tag XL.void attrs out tab
 
 and exp_proj st e lenv out tab =