Remove obsolete FIXME.

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.