- | 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
+ | B.Bind (y, B.Abst (false, n, w), t) ->
+ let i = tsteps m in
+IFDEF SUMMARY THEN
+ if !G.summary then O.add ~x:i ()
+ELSE () END;
+ let n = if i = 0 then n else N.minus st n i in
+ let r = B.Bind (y, B.Abst (true, n, w), t) in
+ step st m r
+ | B.Bind (y, B.Abst (true, n, w), t) ->
+ if !G.si || N.is_not_zero st n then begin match m.s with