diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v index c47270dadea35e5569d63fa7f520d833cc09bc49..042948250904c593ab1d385111d45017a218c3e0 100644 --- a/theories/tests/proofmode.v +++ b/theories/tests/proofmode.v @@ -122,7 +122,7 @@ Proof. iExists {[ 1%positive ]}, ∅. auto. Qed. Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P. Proof. iIntros "H". - (* FIXME: this unshelve should not be needed. *) + (* FIXME: this [unshelve] and [apply _] should not be needed. *) unshelve iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅); try apply _. done. Qed.