X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fdual_rg%2FdrgAut.ml;h=3b371afd72a5371a2804d4b623ad4df36f6e2d0f;hb=552427acaacc2ebd0737c2b6038085f7ea5f423b;hp=c978c4a636fe4c1b1e8a0bbf0c8a7d82dfa813c3;hpb=099f9169edb36348a13f85ebe71c39d44703a696;p=helm.git

diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml
index c978c4a63..3b371afd7 100644
--- a/helm/software/lambda-delta/dual_rg/drgAut.ml
+++ b/helm/software/lambda-delta/dual_rg/drgAut.ml
@@ -108,7 +108,7 @@ let rec xlate_term f st lenv = function
    | A.Abst (name, w, t) ->
       let f ww = 
          let b = mk_abst name ww in
-	 let f tt = f (D.Bind (b, tt)) in
+	 let f tt = f (D.Bind ([b], tt)) in
          xlate_term f st (b :: lenv) t
       in
       xlate_term f st lenv w
@@ -160,7 +160,7 @@ let xlate_entity f st = function
       let f cnt = 
          let f qid = 
             let f ww =
-               let b = D.Abst ([], D.Proj ([], cnt, ww)) in
+               let b = D.Abst ([], D.Bind (cnt, ww)) in
 	       let entry = st.line, uri_of_qid qid, b in
 	       H.add st.henv (uri_of_qid qid) cnt;
 	       f {st with line = succ st.line} (Some entry)
@@ -175,7 +175,7 @@ let xlate_entity f st = function
          let f qid = 
             let f ww vv = 
 	       let a = if trans then [] else [D.Priv] in
-	       let b = D.Abbr (a, D.Proj ([], cnt, D.Cast ([], ww, vv))) in
+	       let b = D.Abbr (a, D.Bind (cnt, D.Cast ([], ww, vv))) in
 	       let entry = st.line, uri_of_qid qid, b in
 	       H.add st.henv (uri_of_qid qid) cnt;
 	       f {st with line = succ st.line} (Some entry)