From a8c1821af86a5524795750feee6c522c91fd7481 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Feb 2016 22:09:58 +0100
Subject: [PATCH] Remove outdated TODO.

---
 heap_lang/heap.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 3c3140a96..134493677 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 ]}.
-- 
GitLab