- | D.Abst ws ->
- let e = D.push_bind C.start e a (D.Abst []) in
- let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
- X.tag X.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
- let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
- X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
- | D.Void n ->
- let attrs = [X.name a; X.mark a; X.arity n] in
- X.tag X.void attrs out tab
+ | 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 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 ->
+ let attrs = [XL.name a; XL.mark a; XL.arity n] in
+ XL.tag XL.void attrs out tab