test-suite/bugs/closed/bug_3562.v


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.