last commit for helena 0.8.1

[helm.git] / helm / software / lambda-delta / src / basic_ag / bagCrg.ml

diff --git a/helm/software/lambda-delta/src/basic_ag/bagCrg.ml b/helm/software/lambda-delta/src/basic_ag/bagCrg.ml
index dcc495232f77181cea5ab6e05847bc435b891d96..8fbf7cf79a609e3a7aa8826c12301125ae9de60a 100644 (file)
--- a/helm/software/lambda-delta/src/basic_ag/bagCrg.ml
+++ b/helm/software/lambda-delta/src/basic_ag/bagCrg.ml
@@ -42,6 +42,7 @@ let rec xlate_term xlate_bind f c = function
       xlate_term xlate_bind f c t
    | D.TProj (_, e, t)  ->
       xlate_term xlate_bind f c (D.tshift e t)
+(* this case should be removed by improving alpha-conversion *)
    | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
       xlate_term xlate_bind f c (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)  ->