X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgReduction.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgReduction.ml;h=c4b2e9c15e7d0ed8104e4e889d0865c6336d56f5;hb=cee0c3ca597ebbff2250674c255ed1bc909521fb;hp=5f73a4fc0e3901c1fc7037612cef1c30fc07efe0;hpb=30bbfa78612ca1ad0c131a75d7075cfd35bebbe1;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
index 5f73a4fc0..c4b2e9c15 100644
--- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
@@ -114,7 +114,7 @@ let rec step st m x =
       begin match m.s with
          | []          -> m, None, x
 	 | (c, v) :: s ->
-            if N.is_zero n then Q.add_infinite st.S.cc a;
+            if N.is_zero n then Q.add_nonzero st.S.cc a;
 	    O.add ~beta:1 ~upsilon:(List.length s) ();
 	    let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in 
 	    step st {m with e = e; s = s} t
@@ -159,13 +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)
-	 when n1 = n2 || st.S.si                               ->
+        _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2)            ->
+	 if n1 = n2 then () else Q.add_equal st.S.cc a1 a2;
 	 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                           ->
+      | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t)    ->
+         if N.is_zero n then () else Q.add_zero st.S.cc a;
 	 O.add ~si:1 ();
 	 ac st (push m1 a b) u (push m2 a b) t
       | _                                                      -> false