last commit for helena 0.8.1

[helm.git] / helm / software / lambda-delta / src / basic_rg / brgCrg.ml

diff --git a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
index 490125095f62118906403cd28c8fcb146f77b6af..8514de641d204c35a1d0d41c1925b38cb3ddac1f 100644 (file)
--- a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
@@ -32,8 +32,6 @@ let rec xlate_term f = function
       xlate_term f t
    | D.TProj (_, e, t)  -> 
       xlate_term f (D.tshift e t)
-   | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
-      xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
    | D.TBind (a, b, t)  ->
       let f tt = f (xlate_bind tt a b) in xlate_term f t