- some bugfix

[helm.git] / helm / software / lambda-delta / src / basic_rg / brgReduction.ml

diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
index 79ffcb32f6b60160dfc24cdce1799a035986a861..5f73a4fc0e3901c1fc7037612cef1c30fc07efe0 100644 (file)
--- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
@@ -159,12 +159,13 @@ let rec ac_nfs st (m1, r1, u) (m2, r2, t) =
          O.add ~gdelta:1 ();
         ac_nfs st (step st m1 v1) (m2, r2, t)             
       | _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1), 
-        _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2)            ->
-        if n1 = n2 && ac {st with S.si = false} m1 w1 m2 w2 then
+        _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2)
+        when n1 = n2 || st.S.si                               ->
+        if ac {st with S.si = false} m1 w1 m2 w2 then
            ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
         else false
       | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t)
-         when N.is_zero n && st.S.si                           ->
+         when N.is_zero n || st.S.si                           ->
         O.add ~si:1 ();
         ac st (push m1 a b) u (push m2 a b) t
       | _                                                      -> false