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) ->
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 =