X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fdual_rg%2FdrgAut.ml;h=4b17faaa110ab5ac1e35a891b9620fc6c8b3bf97;hb=0bcc03be833e8f177850e6b9785713d7975ee8bd;hp=aa6cf5d9766649c92d474caa2f4ac18b14925fb1;hpb=8e40e8ece45938cb8b35d2a997bf50786af5f4df;p=helm.git

diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml
index aa6cf5d97..4b17faaa1 100644
--- a/helm/software/lambda-delta/dual_rg/drgAut.ml
+++ b/helm/software/lambda-delta/dual_rg/drgAut.ml
@@ -132,9 +132,9 @@ let rec xlate_term f st lenv = function
       let map2 f = xlate_term f st lenv in
       let g qid (a, _) =
          let gref = D.TGRef ([], uri_of_qid qid) in
-	 match args with
-	    | []   -> f gref
-	    | args -> 
+	 match args, a with
+	    | [], [] -> f gref
+	    | _      -> 
 	       let f args = f (D.TAppl ([], args, gref)) in
 	       let f args = f (List.rev_map (map2 C.start) args) in
 	       let f a = C.list_rev_map_append f map1 a ~tail:args in
@@ -176,7 +176,14 @@ let xlate_entity err f st = function
 	 let f qid = 
             let ww = xlate_term C.start st lenv w in
 	    H.add henv (uri_of_qid qid) cnt;
-	    let b = Y.Abst (D.TBind (a, D.Abst ws, ww)) in
+	    let t = match ws with
+	       | [] -> ww
+	       | _  -> D.TBind (a, D.Abst ws, ww)
+	    in
+(*
+	    DrgOutput.pp_term print_string t; print_newline ();
+*)
+	    let b = Y.Abst t in
 	    let entity = [Y.Mark st.line], uri_of_qid qid, b in
 	    f {st with line = succ st.line} entity
 	 in
@@ -191,7 +198,14 @@ let xlate_entity err f st = function
             let ww = xlate_term C.start st lenv w in
 	    let vv = xlate_term C.start st lenv v in
 	    H.add henv (uri_of_qid qid) cnt;
-            let b = Y.Abbr (D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))) in
+            let t = match ws with
+	       | [] -> D.TCast ([], ww, vv)
+	       | _  -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))
+	    in
+(*
+            Printf.printf "%s\n" (U.string_of_uri (uri_of_qid qid));
+*)
+	    let b = Y.Abbr t in
 	    let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
 	    let entity = a, uri_of_qid qid, b in
 	    f {st with line = succ st.line} entity