- let f c = f {m with c = c; i = i} in
- B.push f m.c ~c:m.c b
-
-let rec ac_nfs f ~si r m1 a1 u m2 a2 t =
- log2 "Now converting nfs" m1.c u m2.c t;
- match a1, u, a2, t with
- | _, B.Sort (_, h1), _, B.Sort (_, h2) ->
- if h1 = h2 then f r else f false
- | Some (e1, B.Abst _), _, Some (e2, B.Abst _), _ ->
- if e1 = e2 then ac_stacks f r m1 m2 else f false
- | Some (e1, B.Abbr (_, v1)), _, Some (e2, B.Abbr (_, v2)), _ ->
+ let e = B.push m.e m.e a b in
+ {m with e = e; d = d}
+
+let rec ac_nfs st (m1, r1, u) (m2, r2, t) =
+ log2 "Now converting nfs" m1.e u m2.e t;
+ match r1, u, r2, t with
+ | _, B.Sort (_, h1), _, B.Sort (_, h2) ->
+ h1 = h2
+ | Some (e1, _, B.Abst _), _, Some (e2, _, B.Abst _), _ ->
+ if e1 = e2 then ac_stacks st m1 m2 else false
+ | Some (e1, _, B.Abbr v1), _, Some (e2, _, B.Abbr v2), _ ->