X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fxml%2FxmlCrg.ml;h=7b5dd8ddc5b65538befee7e3c687b140ea021bf0;hb=22fd9c98a22929f0319286c0693fcdaee43a72df;hp=a0b5a7f1a3745f2aa04a3b8a6c57c079ee9b5204;hpb=39b42ed90bc74c8b6293842f1ac4aca60fc0c37e;p=helm.git

diff --git a/helm/software/lambda-delta/src/xml/xmlCrg.ml b/helm/software/lambda-delta/src/xml/xmlCrg.ml
index a0b5a7f1a..7b5dd8ddc 100644
--- a/helm/software/lambda-delta/src/xml/xmlCrg.ml
+++ b/helm/software/lambda-delta/src/xml/xmlCrg.ml
@@ -90,15 +90,15 @@ and exp_bind e a b out tab =
    let f a ns = a, ns in
    let a, ns = Y.get_names f a in 
    match b with
-      | D.Abst ws ->
-	 let e = D.push_bind C.start e a (D.Abst []) in
-	 let attrs = [XL.name ns; XL.mark a; XL.arity (List.length ws)] in
+      | D.Abst (n, ws) ->
+	 let e = D.push_bind C.start e a (D.Abst (n, ws)) in
+	 let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity (List.length ws)] in
          XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
-      | D.Abbr vs ->
-         let e = D.push_bind C.start e a (D.Abbr []) in
+      | D.Abbr vs      ->
+         let e = D.push_bind C.start e a (D.Abbr vs) in
          let attrs = [XL.name ns; XL.mark a; XL.arity (List.length vs)] in
          XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
-      | D.Void n ->
+      | D.Void n       ->
          let attrs = [XL.name a; XL.mark a; XL.arity n] in
          XL.tag XL.void attrs out tab