-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 a c m1 t1 m2 t2 =
+(* L.warn "entering R.are_convertible"; *)
+ let rec aux m1 r1 m2 r2 =
+(* L.warn "entering R.are_convertible_aux"; *)
+ 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 a else f false
+ | LRef_ (i1, _), LRef_ (i2, _) ->
+ if i1 = i2 then are_convertible_stacks f a c m1 m2 else f false
+ | GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _) ->
+ if a1 = a2 then are_convertible_stacks f a c m1 m2 else f false
+ | GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) ->
+ if a1 = a2 then
+ let f a = if a then f a else are_convertible f true c m1 v1 m2 v2 in
+ are_convertible_stacks f a c m1 m2
+ else