From 9a940748aca51ae28f1ca58a1cb2deadfa3dfcb1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Nov 2023 12:28:51 +0100
Subject: [PATCH] Add test case.

---
 tests/proofmode.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index f652db7e6..18facf92c 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1602,6 +1602,15 @@ Proof.
   Fail iIntros (? x).
 Abort.
 
+(* See issue #551 *)
+Lemma test_iSpecialize_without_eta {A} (Φ : A → PROP) x :
+  bi_forall Φ ⊢ Φ x.
+Proof.
+  iIntros "H".
+  iSpecialize ("H" $! x).
+  done.
+Qed.
+
 End tests.
 
 Section parsing_tests.
-- 
GitLab