- bug fix in the RTM

[helm.git] / helm / software / helena / src / basic_rg / brgReduction.ml

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index e20737ec4c04fcc4147ece4c1dd195d6ffb9295d..6f9f5f09f1e5e4005b88dfd412d7dfc57b5415dd 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -140,11 +140,11 @@ let rec step st m x =
    | B.Appl (_, v, t)             ->
       step st {m with s = (m.e, v) :: m.s} t   
    | B.Bind (a, B.Abst (n, w), t) ->
+      let i = tsteps m in
+      let n = if i = 0 then n else N.minus st n i in
       if !G.si || N.is_not_zero st n then begin match m.s with
          | []          ->
-            let i = tsteps m in
             if i = 0 then m, x, None else
-            let n = N.minus st n i in
             m, B.Bind (a, B.Abst (n, w), t), None
         | (c, v) :: s ->
             if !G.cc && not (N.assert_not_zero st n) then assert false;