- bug fix in the static analyzer allows better Pi/forall separation (exportation...

[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 b5e3b9b40b7a16058ba1a63a4559847bdf002591..b04f5f6e15ef7a406a50f17ffbe0d558d76960e3 100644 (file)
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -22,7 +22,7 @@ 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
@@ -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.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
@@ -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.kind a] in
+      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         ->
       let attrs = [XL.name a] in