-let rec are_convertible f xl c m1 t1 m2 t2 =
- let rec aux m1 r1 m2 r2 = match r1, r2 with
- | Sort_ h1, Sort_ h2 ->
- if h1 = h2 then f xl else f None
+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