-let rec are_convertible f c m1 t1 m2 t2 =
- let rec aux m1 r1 m2 r2 = match r1, r2 with
- | Sort_ h1, Sort_ h2 -> f (h1 = h2)
- | LRef_ (i1, _), LRef_ (i2, _) ->
- if i1 = i2 then are_convertible_stacks f c m1 m2 else f false
- | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _) ->
- if a1 = a2 then are_convertible_stacks f c m1 m2 else f false
- | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) ->
- if a1 = a2 then are_convertible_stacks f c m1 m2 else
+let rec are_convertible f xl c m1 t1 m2 t2 =
+ let rec aux m1 r1 m2 r2 =
+ let u, t = term_of_whdr r1, term_of_whdr r2 in
+ log2 "Now really converting" c u t;
+ match r1, r2 with
+ | Sort_ h1, Sort_ h2 ->
+ if h1 = h2 then f xl else f None
+ | LRef_ (i1, _), LRef_ (i2, _) ->
+ 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