aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2447.v
blob: fdeb69fcc7b7d85028b87eca5ea7ec765ae42f2e (plain)
1
2
3
4
5
6
7
Record t := {x : bool; y : bool; z : bool}.

Goal forall x1 x2 y z,
  {| x := x1; y := y; z := z |} = {| x := x2; y := y; z := z |} -> x1 = x2.
Proof.
intros; congruence. (* was doing stack overflow *)
Qed.