aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3625.v
blob: d4b2cc5cccdd479034ba8cfbafb8aa2960b0b32a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
Require Import TestSuite.admit.
Set Implicit Arguments.
Set Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }.

Goal forall x y : prod Set Set, x.(@fst _ _) = y.(@fst _ _).
 intros.
 refine (f_equal _ _).
 Undo.
 apply f_equal.
 admit.
Qed.