-and xlate_bind x a b =
- let f a ns = a, ns in
- let a, ns = E.get_names f a in
- match b with
- | D.Abst (m, ws) ->
- let map x n w =
- let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst (m, ww), x) in
- xlate_term f w
- in
- List.fold_left2 map x ns ws
- | D.Abbr vs ->
- let map x n v =
- let f vv = B.Bind (n :: a, B.Abbr vv, x) in
- xlate_term f v
- in
- List.fold_left2 map x ns vs
- | D.Void _ ->
- let map x n = B.Bind (n :: a, B.Void, x) in
- List.fold_left map x ns
+and xlate_bind f y b t = match b with
+ | D.Abst (r, n, w) ->
+ let f ww = f (B.Bind (y, B.Abst (r, n, ww), t)) in
+ xlate_term f w
+ | D.Abbr v ->
+ let f vv = f (B.Bind (y, B.Abbr vv, t)) in
+ xlate_term f v
+ | D.Void ->
+ f (B.Bind (y, B.Void, t))