1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3664.v b/test-suite/bugs/closed/3664.v
new file mode 100644
index 00000000..41de74ff
--- /dev/null
+++ b/test-suite/bugs/closed/3664.v
@@ -0,0 +1,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.
+\ No newline at end of file