]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgReduction.ml
new intermediate language complete_rg,
[helm.git] / helm / software / helena / src / basic_rg / brgReduction.ml
index c3ef9795b6d6f256c08a2726e3f24071b29e308d..09e262d12eb900caa58f02e4e825df3e4d6c69c2 100644 (file)
@@ -181,7 +181,7 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
          let e2 = E.apix C.err C.start a2 in
         if e1 = e2 then ac_stacks st m1 m2 else false
       | B.GRef (_, u1), None, B.GRef (_, u2), None          ->
-        if U.eq u1 u2 & assert_iterations m1 m2 then ac_stacks st m1 m2 else false
+        if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
       | B.GRef (a1, u1), Some v1, B.GRef (a2, u2), Some v2  ->
          let e1 = E.apix C.err C.start a1 in
          let e2 = E.apix C.err C.start a2 in
@@ -191,7 +191,7 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
         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
+         end else if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
          else begin
            if !G.summary then O.add ~gdelta:2 ();
            ac st m1 v1 m2 v2