- | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
- xlate_term xlate_bind f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
- | D.TBind (a, b, t) ->
- let g _ ns = ns in
- let ns = E.get_names g a in
- let cc = xlate_bind C.start c ns b in
- let f tt = f (shift tt (cc, ns)) in
- xlate_term xlate_bind f cc t
-
-let rec xlate_bind f c ns = function
- | D.Abst (_, ws) ->
- let map f n w c =
- let f ww = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abst ww) in
- xlate_term xlate_bind f c w
+ | D.TBind (y, D.Abst (x, n, ws), D.TCast (u, t)) ->
+ xlate_term st f c (D.TCast (D.TBind (y, D.Abst (x, N.minus st n 1, ws), u), D.TBind (y, D.Abst (x, n, ws), t)))
+ | D.TBind (y, b, t) ->
+ let f cc =
+ let a, l, b = List.hd cc in
+ let f tt = f (Z.Bind (a, l, b, tt)) in
+ xlate_term st f cc t