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
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