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.
|
