new options activated

[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 f04930851035d2d323499eef96a046e0477a5f2d..b5e3b9b40b7a16058ba1a63a4559847bdf002591 100644 (file)
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -27,9 +27,9 @@ let lenv_iter map_bind map_appl map_proj st e lenv out tab =
 (* 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)
@@ -61,9 +61,9 @@ 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 (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,9 +75,9 @@ 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) ->