X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fdual_rg%2FdrgBrg.ml;h=1f149a759f9ce2cd621bb82a31991b80b8153e86;hb=be1700416b160f793c0368a39600b7f81bfb2e44;hp=2510f892056bc14a6c6c2a00aaa375e7d6f235cc;hpb=e3fc33cab9b7736c6475cf2c9cd7f91c5a4bd7f9;p=helm.git

diff --git a/helm/software/lambda-delta/dual_rg/drgBrg.ml b/helm/software/lambda-delta/dual_rg/drgBrg.ml
index 2510f8920..1f149a759 100644
--- a/helm/software/lambda-delta/dual_rg/drgBrg.ml
+++ b/helm/software/lambda-delta/dual_rg/drgBrg.ml
@@ -39,7 +39,23 @@ let rec xlate_term f = function
    | 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