X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgCrg.ml;h=984f84916a26e3ff434c9202d6500b0ca13752bf;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=645610dd44f4c62db2570a2d2d5888b0904a9ee3;hpb=67686e04702688cc822e809e5168f765bf69d7cb;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml
index 645610dd4..984f84916 100644
--- a/helm/software/helena/src/basic_rg/brgCrg.ml
+++ b/helm/software/helena/src/basic_rg/brgCrg.ml
@@ -18,48 +18,48 @@ module B = Brg
 (* internal functions: crg to brg term **************************************)
 
 let rec xlate_term f = function
-   | D.TSort (a, l)       -> f (B.Sort (a, l))
-   | D.TGRef (a, n)       -> f (B.GRef (a, n))
-   | D.TLRef (a, i)       -> f (B.LRef (a, i))
-   | D.TCast (a, u, t)    ->
-      let f tt uu = f (B.Cast (a, uu, tt)) in
+   | D.TSort k         -> f (B.Sort k)
+   | D.TGRef (a, n)    -> f (B.GRef (a, n))
+   | D.TLRef (a, i)    -> f (B.LRef (a, i))
+   | D.TCast (u, t)    ->
+      let f tt uu = f (B.Cast (uu, tt)) in
       let f tt = xlate_term (f tt) u in
-      xlate_term f t 
-   | D.TAppl (a, x, v, t) ->
-      let f tt vv = f (B.Appl (a, x, vv, tt)) in
+      xlate_term f t
+   | D.TAppl (a, v, t) ->
+      let f tt vv = f (B.Appl (a, vv, tt)) in
       let f tt = xlate_term (f tt) v in
       xlate_term f t 
-   | D.TProj (_, e, t)    -> 
+   | D.TProj (e, t)    -> 
       D.shift (xlate_term f) e t
-   | D.TBind (a, b, t)    -> 
-      xlate_term (xlate_bind f a b) t
+   | D.TBind (y, b, t)    -> 
+      xlate_term (xlate_bind f y b) t
 
-and xlate_bind f a b t = match b with
+and xlate_bind f y b t = match b with
    | D.Abst (r, n, w) ->
-      let f ww = f (B.Bind (a, B.Abst (r, n, ww), t)) in 
+      let f ww = f (B.Bind (y, B.Abst (r, n, ww), t)) in 
       xlate_term f w
    | D.Abbr v         ->
-      let f vv = f (B.Bind (a, B.Abbr vv, t)) in 
+      let f vv = f (B.Bind (y, B.Abbr vv, t)) in 
       xlate_term f v
    | D.Void           ->
-      f (B.Bind (a, B.Void, t))
+      f (B.Bind (y, B.Void, t))
 
 (* internal functions: brg to crg term **************************************)
 
 let rec xlate_bk_term f = function
-   | B.Sort (a, l)       -> f (D.TSort (a, l))
-   | B.GRef (a, n)       -> f (D.TGRef (a, n))
-   | B.LRef (a, i)       -> f (D.TLRef (a, i))
-   | B.Cast (a, u, t)    ->
-      let f tt uu = f (D.TCast (a, uu, tt)) in
+   | B.Sort k         -> f (D.TSort k)
+   | B.GRef (a, n)    -> f (D.TGRef (a, n))
+   | B.LRef (a, i)    -> f (D.TLRef (a, i))
+   | B.Cast (u, t)    ->
+      let f tt uu = f (D.TCast (uu, tt)) in
       let f tt = xlate_bk_term (f tt) u in
       xlate_bk_term f t 
-   | B.Appl (a, x, u, t) ->
-      let f tt uu = f (D.TAppl (a, x, uu, tt)) in
+   | B.Appl (a, u, t) ->
+      let f tt uu = f (D.TAppl (a, uu, tt)) in
       let f tt = xlate_bk_term (f tt) u in
       xlate_bk_term f t 
-   | B.Bind (a, b, t)    ->
-      let f tt bb = f (D.TBind (a, bb, tt)) in
+   | B.Bind (y, b, t) ->
+      let f tt bb = f (D.TBind (y, bb, tt)) in
       let f tt = xlate_bk_bind (f tt) b in
       xlate_bk_term f t