aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Decompose.v
blob: 1316cbf957d542743ab25ab793d3383a1346f824 (plain)
1
2
3
4
5
6
7
8
9
(* This was a Decompose bug reported by Randy Pollack (29 Mar 2000) *)

Goal
0 = 0 /\ (forall x : nat, x = x -> x = x /\ (forall y : nat, y = y -> y = y)) ->
True.
intro H.
decompose [and] H. (* Was failing *)

Abort.