| A.Abst (name, w, t) ->
let f ww =
let b = mk_abst name ww in
- let f tt = f (D.Bind (b, tt)) in
+ let f tt = f (D.Bind ([b], tt)) in
xlate_term f st (b :: lenv) t
in
xlate_term f st lenv w
let f cnt =
let f qid =
let f ww =
- let b = D.Abst ([], D.Proj ([], cnt, ww)) in
+ let b = D.Abst ([], D.Bind (cnt, ww)) in
let entry = st.line, uri_of_qid qid, b in
H.add st.henv (uri_of_qid qid) cnt;
f {st with line = succ st.line} (Some entry)
let f qid =
let f ww vv =
let a = if trans then [] else [D.Priv] in
- let b = D.Abbr (a, D.Proj ([], cnt, D.Cast ([], ww, vv))) in
+ let b = D.Abbr (a, D.Bind (cnt, D.Cast ([], ww, vv))) in
let entry = st.line, uri_of_qid qid, b in
H.add st.henv (uri_of_qid qid) cnt;
f {st with line = succ st.line} (Some entry)