aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_3562.v
blob: bdb3fcb65ff8e5c11b7d57ea652834640d837a37 (plain)
1
2
3
4
5
6
7
(* Should not be an anomaly as it was at some time in
   September/October 2014 but some "Disjunctive/conjunctive
   introduction pattern expected" error *)

Theorem t: True.
Fail destruct 0 as x.
Abort.