last commit for helena 0.8.2

[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 6f9f5f09f1e5e4005b88dfd412d7dfc57b5415dd..9a14a11fb6fd29b34af6d13aa56fb50d43e2dd07 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -208,9 +208,9 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
         ac_nfs st (step st m1 v1) (m2, t2, r2)
       | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _, 
         B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _  ->
-        if !G.cc && not (N.assert_equal st n1 n2) then false else
-         if ac st (reset m1 zero) w1 (reset m2 zero) w2 then
-           ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
+        if ((!G.cc && N.assert_equal st n1 n2) || N.are_equal st n1 n2) &&
+            ac st (reset m1 zero) w1 (reset m2 zero) w2
+         then ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
         else false
       | B.Sort _, _, B.Bind (a, B.Abst (n, _), t), _ ->
          if !G.si then