aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened/3794.v
blob: e4711a38c0047b4851071fe0978530293155e0ea (plain)
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.
Fail typeclasses eauto with core.
Abort.