X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgReduction.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgReduction.ml;h=98747ab55a810f10ee463d28cb8270f56dd16a76;hb=651d745df2454a9e232aff3c9d8bf3e77653936d;hp=c4b2e9c15e7d0ed8104e4e889d0865c6336d56f5;hpb=fb6fee82bb9172e15b1a7bc7e20641627f593fcc;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
index c4b2e9c15..98747ab55 100644
--- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
@@ -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