+ | B.Bind (b, t) ->
+ P.add ~upsilon:(List.length m.s) ();
+ let f c = step f ~delta ~rt {m with c = c} t in
+ B.push f m.c ~c:m.c b
+
+let push f m b =
+ assert (m.s = []);
+ let b, i = match b with
+ | B.Abst (a, w) -> B.abst (Y.Apix m.i :: a) w, succ m.i
+ | b -> b, m.i
+ in
+ let f c = f {m with c = c; i = i} in
+ B.push f m.c ~c:m.c b
+
+let rec ac_nfs err f ~si 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 () else err ()
+ | Some (e1, B.Abst _), _, Some (e2, B.Abst _), _ ->
+ if e1 = e2 then ac_stacks err f m1 m2 else err ()
+ | Some (e1, B.Abbr (_, v1)), _, Some (e2, B.Abbr (_, v2)), _ ->
+ if e1 = e2 then
+ let err _ = P.add ~gdelta:2 (); ac err f ~si m1 v1 m2 v2 in
+ ac_stacks err f m1 m2
+ else if e1 < e2 then begin
+ P.add ~gdelta:1 ();
+ step (ac_nfs err f ~si m1 a1 u) m2 v2
+ end else begin
+ P.add ~gdelta:1 ();
+ step (ac_nfs_rev err f ~si m2 a2 t) m1 v1
+ end
+ | _, _, Some (_, B.Abbr (_, v2)), _ ->
+ P.add ~gdelta:1 ();
+ step (ac_nfs err f ~si m1 a1 u) m2 v2
+ | Some (_, B.Abbr (_, v1)), _, _, _ ->
+ P.add ~gdelta:1 ();
+ step (ac_nfs_rev err f ~si m2 a2 t) m1 v1
+ | _, B.Bind ((B.Abst (_, w1) as b1), t1),
+ _, B.Bind ((B.Abst (_, w2) as b2), t2) ->
+ let f m1 m2 = ac err f ~si m1 t1 m2 t2 in
+ let f m1 = push (f m1) m2 b2 in
+ let f _ = push f m1 b1 in
+ ac err f ~si:false m1 w1 m2 w2
+ | _, B.Sort _, _, B.Bind (b, t) when si ->
+ P.add ~si:1 ();
+ let f m1 m2 = ac err f ~si m1 u m2 t in
+ let f m1 = push (f m1) m2 b in
+ push f m1 b
+ | _ -> err ()
+
+and ac_nfs_rev err f ~si m2 a2 t m1 a1 u = ac_nfs err f ~si m1 a1 u m2 a2 t
+
+and ac err f ~si m1 t1 m2 t2 =
+(* L.warn "entering R.are_convertible"; *)
+ let f m1 a1 t1 = step (ac_nfs err f ~si m1 a1 t1) m2 t2 in
+ step f m1 t1
+
+and ac_stacks err f m1 m2 =
+(* L.warn "entering R.are_convertible_stacks"; *)
+ if List.length m1.s <> List.length m2.s then err () else
+ let map f (c1, v1) (c2, v2) =
+ let m1, m2 = {m1 with c = c1; s = []}, {m2 with c = c2; s = []} in
+ ac err f ~si:false m1 v1 m2 v2
+ in
+ C.list_iter2 f map m1.s m2.s