X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgCrg.ml;h=984f84916a26e3ff434c9202d6500b0ca13752bf;hp=a7064d07439532a5d9107e9ab7b5978a2eebb800;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hpb=fdb80b08af83b86759833142456ce3c4f84cd80e diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml index a7064d074..984f84916 100644 --- a/helm/software/helena/src/basic_rg/brgCrg.ml +++ b/helm/software/helena/src/basic_rg/brgCrg.ml @@ -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) ->