aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3596.v
blob: 49dd7be5a88a749277761f5b2f1b928e4d157e3d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Require Import TestSuite.admit.
Set Implicit Arguments.
Record foo := { fx : nat }.
Set Primitive Projections.
Record bar := { bx : nat }.
Definition Foo (f : foo) : f = f.
  destruct f as [fx]; destruct fx; admit.
Defined.
Definition Bar (b : bar) : b = b.
  destruct b as [fx]; destruct fx; admit.
Defined.
Goal forall f b, Bar b = Bar b -> Foo f = Foo f.
  intros f b.
  destruct f, b. 
  simpl.
  Fail progress unfold Bar. (* success *)
  Fail progress unfold Foo. (* failed to progress *)
  reflexivity.
Qed.