aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3054.v
blob: 936e58e1977d70745a5bc890070fad7fe75f243f (plain)
1
2
3
4
5
6
7
8
9
10
Section S.

Let V := Type.

Goal ~ true = false.
Proof.
congruence.
Qed.

End S.