- XL.tag XL.appl attrs ~contents:(exp_term e v) out tab;
- exp_term e t out tab
- | D.TProj (a, lenv, t) ->
+ XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
+ exp_term st e t out tab
+ | D.TAppl (a, v, t) ->
+ let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in
+ XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
+ exp_term st e t out tab
+ | D.TProj (lenv, t) ->