]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgCrg.ml
update in helena
[helm.git] / helm / software / helena / src / basic_rg / brgCrg.ml
index a7064d07439532a5d9107e9ab7b5978a2eebb800..984f84916a26e3ff434c9202d6500b0ca13752bf 100644 (file)
@@ -25,8 +25,8 @@ let rec xlate_term f = function
       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 (x, v, t) ->
-      let f tt vv = f (B.Appl (x, vv, tt)) in
+   | 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)    -> 
@@ -54,8 +54,8 @@ let rec xlate_bk_term f = function
       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 (x, u, t) ->
-      let f tt uu = f (D.TAppl (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 (y, b, t) ->