test-suite/bugs/closed/3402.v


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.