X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgReduction.ml;h=08f3a340756e8187297fa966e38e54e5394f1b36;hb=2dc6df301ca3ebf444ec7f767921ee0e57ccd592;hp=002f12ce11e028bf01dcbc7e89b1c7c9add21a29;hpb=bbc1c6ccb596693c46f4d75d7875b94c79f1d575;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index 002f12ce1..08f3a3407 100644
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -140,11 +140,7 @@ 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) ->
-(*      if not !G.cc && st.S.si && N.to_string st.S.lenv n = "0" then begin
-         if !G.summary then O.add ~upsilon:1 ();
-         let e = B.push m.e m.e a B.Void in 
-         step st {m with e = e} t
-      end else *) begin match m.s with
+      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
@@ -156,6 +152,10 @@ let rec step st m x =
 	    let v = if assert_tstep m false then B.Cast (E.empty_node, w, v) else v in
             let e = B.push m.e c a (B.abbr v) in
 	    step st {m with e = e; s = s} t
+      end else begin
+         if !G.summary then O.add ~upsilon:1 ();
+         let e = B.push m.e m.e a B.Void in 
+         step st {m with e = e} t
       end
    | B.Bind (a, b, t)        ->
       if !G.summary then O.add ~theta:(List.length m.s) ();