]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/dual_rg/drgAut.ml
xml: first ld to xml stylesheets
[helm.git] / helm / software / lambda-delta / dual_rg / drgAut.ml
index c978c4a636fe4c1b1e8a0bbf0c8a7d82dfa813c3..3b371afd72a5371a2804d4b623ad4df36f6e2d0f 100644 (file)
@@ -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)