- let f ww vv =
- H.add st.henv (uri_of_qid qid) cnt;
- let b = Y.Abbr (D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))) in
- let a =
- if trans then [Y.Mark st.line] else [Y.Mark st.line; Y.Priv]
- in
- let entity = a, uri_of_qid qid, b in
- f {st with line = succ st.line} entity
+ let ww = xlate_term C.start st lenv w in
+ let vv = xlate_term C.start st lenv v in
+ H.add henv (uri_of_qid qid) cnt;
+ let t = match ws with
+ | [] -> D.TCast ([], ww, vv)
+ | _ -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))