(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* unify x y with typeclass_instances ; fail 1 "Convertible" | |- _ => exact tt end. Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.