]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgReduction.ml
- brgOutput: the nodes count is now implemented
[helm.git] / helm / software / lambda-delta / basic_rg / brgReduction.ml
index 87d093d82f47638ea9580a89996d7f632482e0d6..16dc395bbfe39c7eb6e4c94a1936ae2ff2874705 100644 (file)
@@ -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)        ->