- if i1 = i2 then are_convertible_stacks f xl c m1 m2 else f None
- | GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _) ->
- if a1 = a2 then are_convertible_stacks f xl c m1 m2 else f None
- | GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) ->
- if a1 = a2 then are_convertible_stacks f xl c m1 m2 else
+ if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false
+ | GRef_ ((Y.Apix a1 :: _), _, Y.Abst _),
+ GRef_ ((Y.Apix a2 :: _), _, Y.Abst _) ->
+ if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
+ | GRef_ ((Y.Apix a1 :: _), _, Y.Abbr v1),
+ GRef_ ((Y.Apix a2 :: _), _, Y.Abbr v2) ->
+ if a1 = a2 then
+ let f a =
+ if a then f a else are_convertible f ~si true c m1 v1 m2 v2
+ in
+ are_convertible_stacks f ~si a c m1 m2
+ else