diff --git a/theories/typing/own.v b/theories/typing/own.v
index db4fce97dd7153cefe4a871e96bb396e84e03376..bec0f4a1f7c072345b027f663a2e0456496fd1f2 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -204,8 +204,6 @@ Section util.
          ∃ (l : loc) (vl' : vec val m), ⌜v = #l⌝ ∗ ▷ l ↦∗ vl' ∗ ▷ freeable_sz n m l.
   Proof.
     rewrite ownptr_own. apply uPred.exist_proper=>l. iSplit.
-    (* FIXME: The goals here look rather confusing:  One cannot tell that we are looking at
-       a statement in Iris; the top-level → could just as well be a Coq implication. *)
     - iIntros "H". iDestruct "H" as (vl) "(% & Hl & _ & $)". subst v.
       iExists vl. iSplit; done.
     - iIntros "H". iDestruct "H" as (vl) "(% & Hl & $)". subst v.