diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 3c3140a96a335d943f356fc38e1318cf985ed61e..134493677c101c1b4acb015ce527de21211a4db9 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -15,9 +15,6 @@ Proof. split; apply _. Qed.
 Definition to_heap : state → heapRA := fmap Excl.
 Definition of_heap : heapRA → state := omap (maybe Excl).
 
-(* TODO: Do we want to expose heap ownership based on the state, or the heapRA?
-   The former does not expose the annoying "Excl", so for now I am going for
-   that. We should be able to derive the lemmas we want for this, too. *)
 Definition heap_mapsto {Σ} (i : gid) `{HeapInG Σ i}
     (γ : gname) (l : loc) (v : val) : iPropG heap_lang Σ :=
   auth_own i γ {[ l ↦ Excl v ]}.