Library Coq.Classes.Init
Hints for the proof search: these combinators should be considered rigid.
The unconvertible typeclass, to test that two objects of the same type are
actually different.
Class Unconvertible (
A :
Type) (
a b :
A) :=
unconvertible :
unit.
Ltac unconvertible :=
match goal with
| |- @
Unconvertible _ ?x ?y =>
unify x y with typeclass_instances ;
fail 1 "Convertible"
| |-
_ =>
exact tt
end.
Hint Extern 0 (@
Unconvertible _ _ _) =>
unconvertible :
typeclass_instances.