new semantics of the -g option completed

[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 f20335193e8868dd9ed376e5be5dc8e32c46ab16..35f5f0222a8b2af070e6e0bb382e0a761ce972a9 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -147,9 +147,6 @@ let rec step st m r =
          | []          ->
             m, B.Bind (a, B.Abst (true, n, w), t), None
         | (c, v) :: s ->
-(*
-            if !G.cc && not (N.assert_not_zero st n) then assert false;
-*)
            if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
            let v = B.Cast (E.empty_node, w, v) in
             let e = B.push m.e c a (B.abbr v) in
@@ -190,17 +187,17 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
         if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
       | B.GRef ({E.n_apix = e1}, u1), Some v1, 
         B.GRef ({E.n_apix = e2}, u2), Some v2              ->
-         if e1 < e2 then begin 
+         if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
+         else if e1 < e2 then begin 
             if !G.summary then O.add ~gdelta:1 ();
            ac_nfs st (m1, t1, r1) (step st m2 v2)
         end else if e2 < e1 then begin
            if !G.summary then O.add ~gdelta:1 ();
            ac_nfs st (step st m1 v1) (m2, t2, r2) 
-         end else if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
-         else begin
+         end else begin
            if !G.summary then O.add ~gdelta:2 ();
            ac st m1 v1 m2 v2
-         end 
+         end
       | _, _, B.GRef _, Some v2                            ->
          if !G.summary then O.add ~gdelta:1 ();
         ac_nfs st (m1, t1, r1) (step st m2 v2)