X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fxml%2FxmlCrg.ml;h=311a0b4a1192c3a076dc2dd4a17472b9148c504f;hb=04ffe68396b98bbf21bcd403ffba03b94eaebadc;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..311a0b4a1 100644
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -81,7 +81,7 @@ and exp_appl st e a 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
+      let attrs = [XL.level st n; XL.name a; XL.kind a] in
       XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
    | D.Abbr v      ->
       let attrs = [XL.name a] in