now type inclusion is correctly managed 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 002f12ce11e028bf01dcbc7e89b1c7c9add21a29..08f3a340756e8187297fa966e38e54e5394f1b36 100644 (file)
--- 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) ();