summaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened/3562.v
blob: 04a1223b6edfa19fbc779b8ab0856ecf02c0566a (plain)
1
2
Theorem t: True.
Fail destruct 0 as x.