let t1' = whd t1
and t2' = whd t2 in
debug t1' [t2'] "POSTWHD";
-let res =
match (t1',t2') with
(C.Rel n1, C.Rel n2) -> n1 = n2
| (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
| (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
| (C.Implicit, _) | (_, C.Implicit) ->
raise (Impossible 3) (* we don't trust our whd ;-) *)
- | (_,_) ->
- debug t1' [t2'] "NOT-CONVERTIBLE" ;
- false
-in
-if res then true else (debug t1' [t2'] "NOT-CONVERTIBLE" ; false)
+ | (_,_) -> false
end
in
aux t1 t2