Better error message.

[helm.git] / helm / software / lambda-delta / dual_rg / drgAut.ml

diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml
index aa6cf5d9766649c92d474caa2f4ac18b14925fb1..4b17faaa110ab5ac1e35a891b9620fc6c8b3bf97 100644 (file)
--- 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