aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3562.v
blob: 1a1410a3b1dfb6b3ad60bd67ddcdc41ff023da3d (plain)
1
2
3
4
5
6
(* 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.