test-suite/bugs/closed/bug_8544.v


1
2
3
4
5
6

Require Import ssreflect.
Goal True \/ True -> False.
Proof.
(* the following should fail: 2 subgoals, but only one intro pattern *)
Fail case => [a].
Abort.