]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/basic_rg/brgReduction.ml
first commit for Helena 0.8.2
[helm.git] / helm / software / lambda-delta / src / basic_rg / brgReduction.ml
index c4b2e9c15e7d0ed8104e4e889d0865c6336d56f5..98747ab55a810f10ee463d28cb8270f56dd16a76 100644 (file)
@@ -115,12 +115,12 @@ let rec step st m x =
          | []          -> m, None, x
         | (c, v) :: s ->
             if N.is_zero n then Q.add_nonzero st.S.cc a;
-           O.add ~beta:1 ~upsilon:(List.length s) ();
+           O.add ~beta:1 ~theta:(List.length s) ();
            let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in 
            step st {m with e = e; s = s} t
       end
    | B.Bind (a, b, t)        ->
-      O.add ~upsilon:(List.length m.s) ();
+      O.add ~theta:(List.length m.s) ();
       let e = B.push m.e m.e a b in 
       step st {m with e = e} t