test-suite/bugs/opened/3794.v


1
2
3
4
5
6
7

Hint Extern 10 ((?X = ?Y) -> False) => intros; discriminate.
Hint Unfold not : core.

Goal true<>false.
Set Typeclasses Debug.
typeclasses eauto with core.
Qed.