henv: environment; (* optimized global environment *)
path: D.id list; (* current section path *)
hcnt: environment; (* optimized context *)
node: context_node; (* current context node *)
nodes: context_node list; (* context node list *)
line: int; (* line number *)
henv: environment; (* optimized global environment *)
path: D.id list; (* current section path *)
hcnt: environment; (* optimized context *)
node: context_node; (* current context node *)
nodes: context_node list; (* context node list *)
line: int; (* line number *)
let lenv_of_cnt (a, ws) =
D.push C.start D.empty_lenv a (D.Abst ws)
let lenv_of_cnt (a, ws) =
D.push C.start D.empty_lenv a (D.Abst ws)
let str = String.concat "/" path in
let str = Filename.concat str id in
let f str = f (U.uri_of_string str, id, path) in
let str = String.concat "/" path in
let str = Filename.concat str id in
let f str = f (U.uri_of_string str, id, path) in
let f vv = xlate_term (f vv) st lenv t in
xlate_term f st lenv v
| A.Abst (name, w, t) ->
let f ww =
let a, b = [Y.Name (name, true)], (D.Abst [ww]) in
let f vv = xlate_term (f vv) st lenv t in
xlate_term f st lenv v
| A.Abst (name, w, t) ->
let f ww =
let a, b = [Y.Name (name, true)], (D.Abst [ww]) in
- let f args = f (D.Appl ([], args, D.GRef ([], uri_of_qid qid))) in
+ let f args = f (D.TAppl ([], args, D.TGRef ([], uri_of_qid qid))) in
let entity = [Y.Mark st.line], uri_of_qid qid, b in
f {st with line = succ st.line} entity
in
let entity = [Y.Mark st.line], uri_of_qid qid, b in
f {st with line = succ st.line} entity
in
- let b = Y.Abbr (D.Bind (a, D.Abst ws, D.Cast ([], ww, vv))) in
+ let b = Y.Abbr (D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))) in