let a = E.node_attrs ~sort:h () in
f a (D.TSort (a, h))
| A.Appl (v, t) ->
- let f vv at tt = f at (D.TAppl (at, vv, tt)) in
+ let f vv at tt = f at (D.TAppl (at, !G.extended, vv, tt)) in
let f _ vv = xlate_term (f vv) st lst y lenv t in
xlate_term f st lst false lenv v
| A.Abst (name, w, t) ->
| A.GRef (name, args) ->
let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in
let map2 f arg args =
- let f _ arg = f (D.EAppl (args, E.empty_node, arg)) in
+ let f _ arg = f (D.EAppl (args, E.empty_node, !G.extended, arg)) in
xlate_term f st lst false lenv arg
in
let g qid a cnt =
let gref = D.TGRef (a, uri_of_qid qid) in
if cnt = D.ESort then f a gref else
let f = function
- | D.EAppl (D.ESort, _, v) -> f a (D.TAppl (a, v, gref))
- | args -> f a (D.TProj (a, args, gref))
+ | D.EAppl (D.ESort, _, x, v) -> f a (D.TAppl (a, x, v, gref))
+ | args -> f a (D.TProj (a, args, gref))
in
let f args = C.list_fold_right f map2 args D.ESort in
D.sub_list_strict (D.fold_names f map1 args) cnt args
*)
let b = E.Abst t in
let entity = E.empty_root, aw, uri_of_qid qid, b in
+ G.set_current_trace lst.line;
f {lst with line = succ lst.line} entity
in
xlate_term f st lst true lenv w
let b = E.Abbr t in
let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in
let entity = ra, na, uri_of_qid qid, b in
+ G.set_current_trace lst.line;
f {lst with line = succ lst.line} entity
in
xlate_term f st lst false lenv v