| D.TBind (a, b, t) ->
let f tt = f (xlate_bind tt a b) in xlate_term f t
-and xlate_bind x a b = assert false
+and xlate_bind x a b =
+ let f a ns = a, ns in
+ let a, ns = Y.get_names f a in
+ match b with
+ | D.Abst ws ->
+ let map x n w =
+ let f ww = B.Bind (B.Abst (n :: a, 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 (B.Abbr (n :: a, vv), x) in xlate_term f v
+ in
+ List.fold_left2 map x ns vs
+ | D.Void _ ->
+ let map x n = B.Bind (B.Void (n :: a), x) in
+ List.fold_left map x ns
and xlate_proj x _ e =
lenv_fold_left xlate_bind xlate_proj x e