pp_lenv print_string e; print_string " |- ";
pp_term print_string hd; print_newline ();
*)
- map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
+ map e hd out tab; f (D.push2 C.err C.start e ~attr:n ~t:hd ())
in
aux err f e (ns, tl)
| _ -> err ()
let a, ns = Y.get_names f a in
match b with
| D.Abst (n, ws) ->
- let e = D.push_bind C.start e a (D.Abst (n, ws)) in
+ let e = D.push_bind C.start e a (D.Abst (n, [])) 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 e = D.push_bind C.start e a (D.Abbr []) 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 ->