X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgReduction.ml;h=16dc395bbfe39c7eb6e4c94a1936ae2ff2874705;hb=9f8544610ba0245bde47f367de6716e1f256ab18;hp=87d093d82f47638ea9580a89996d7f632482e0d6;hpb=5d492df3e2715395a554f64dc3f040e13f892974;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 87d093d82..16dc395bb 100644
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -107,7 +107,7 @@ let rec step f ?(delta=false) ?(rt=false) c m x =
             P.add ~beta:1 ~upsilon:(List.length tl) ();
 	    let f mc sc = step f ~delta ~rt c {c = mc; s = sc} t in
 	    let f mc = lift_stack (f mc) tl in 
-	    let f v = B.push f m.c a (B.Abbr (B.Cast ([], w, v))) in
+	    let f v = B.push f m.c a (B.Abbr v (* (B.Cast ([], w, v)) *) ) in
 	    S.lift f h (0) v
       end
    | B.Bind (a, b, t)        ->