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