blob: 41de74ff352eecb41f9a02d7681fd3f8292e6167 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Module NonPrim.
Unset Primitive Projections.
Record c := { d : Set }.
Definition a x := d x.
Goal forall x, a x.
intro x.
Fail progress simpl. (* [progress simpl] fails correctly *)
Fail progress cbn. (* [progress cbn] fails correctly *)
admit.
Defined.
End NonPrim.
Module Prim.
Set Primitive Projections.
Record c := { d : Set }.
Definition a x := d x.
Goal forall x, a x.
intro x.
Fail progress simpl. (* [progress simpl] fails correctly *)
Fail progress cbn. (* [cbn] succeeds incorrectly, giving [d x] *)
admit.
Defined.
End Prim.
|
