aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3402.v
blob: ed47ec8255daa264831c43fe5034521529178d2e (plain)
1
2
3
4
5
6
7
Set Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }.
Goal forall A B (p : prod A B), p = let (x, y) := p in pair A B x y.
Proof.
  intros A B p.
  exact eq_refl.
Qed.