and ac_stacks st m1 m2 =
(* L.warn "entering R.are_convertible_stacks"; *)
-(* if List.length m1.s <> List.length m2.s then false else *)
+ if List.length m1.s <> List.length m2.s then false else
let map (c1, v1) (c2, v2) =
let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in
ac {st with Y.si = false} m1 v1 m2 v2
let are_convertible st mu u mw w =
L.box level; log2 "Now converting" mu.e u mw.e w;
- let r = ac {st with Y.delta = false; Y.rt = false} mu u mw w in
+ let r = ac {st with Y.delta = st.Y.expand; Y.rt = false} mu u mw w in
L.unbox level; r
(* let err _ = in
if S.eq mu mw then are_alpha_convertible err f u w else err () *)