blob: 63a81b6d01514fc571c01ec1b532281b3ab9b484 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
Require Import TestSuite.admit.
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.
|
