summaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened/3626.v
blob: 46a6c009eb4af01a327c7ce764f14116903ea751 (plain)
1
2
3
4
5
6
7
Set Implicit Arguments.
Set Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }.

Fail Goal forall x y : prod Set Set, x.(@fst) = y.(@fst).
(*  intros.
    apply f_equal. *)