aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3266.v
blob: fd4cbff85c04a591788982c61eef87916faad9a2 (plain)
1
2
3
Class A := a : nat.
Lemma p : True.
Proof. cut A; [tauto | exact 1]. Qed.