X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fxml%2FxmlCrg.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fxml%2FxmlCrg.ml;h=3eea8cd8724104d162743ac45949a211712a515d;hb=f7988fc51f7c96617aa2b3320628645480af681a;hp=7b5dd8ddc5b65538befee7e3c687b140ea021bf0;hpb=fa9e69af2ad5a22692f6fdd555d37bc6d80c5ad9;p=helm.git

diff --git a/helm/software/lambda-delta/src/xml/xmlCrg.ml b/helm/software/lambda-delta/src/xml/xmlCrg.ml
index 7b5dd8ddc..3eea8cd87 100644
--- a/helm/software/lambda-delta/src/xml/xmlCrg.ml
+++ b/helm/software/lambda-delta/src/xml/xmlCrg.ml
@@ -73,7 +73,7 @@ let rec exp_term e t out tab = match t with
       XL.tag XL.cast attrs ~contents:(exp_term e u) out tab;
       exp_term e t out tab
    | D.TAppl (a, vs, t)   ->
-      let attrs = [XL.arity (List.length vs)] in
+      let attrs = [XL.arity vs] in
       XL.tag XL.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
       exp_term e t out tab
    | D.TProj (a, lenv, t) ->
@@ -92,14 +92,14 @@ and exp_bind e a b out tab =
    match b with
       | 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
+	 let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity 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 vs) in
-         let attrs = [XL.name ns; XL.mark a; XL.arity (List.length vs)] in
+         let attrs = [XL.name ns; XL.mark a; XL.arity vs] in
          XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
       | D.Void n       ->
-         let attrs = [XL.name a; XL.mark a; XL.arity n] in
+         let attrs = [XL.name a; XL.mark a; XL.arity ~n []] in
          XL.tag XL.void attrs out tab
 
 and exp_eproj e a lenv out tab =