From 676dd4ecc60b063731a18d0e34b31803d2353804 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 6 Mar 2018 13:52:13 +0100
Subject: [PATCH] expand FIXME

---
 theories/tests/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index c47270dad..042948250 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.
 
-- 
GitLab