diff --git a/tests/proofmode.v b/tests/proofmode.v index f652db7e6240da1613aebc7171f1c707555580c8..18facf92c4d0fc278ace0e7dffff4031ea6b702e 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.