From 1747d779f02646ecd9a7a52fb8dadc6516c6ce9d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Apr 2016 12:27:36 +0200
Subject: [PATCH] Remove old todo.

---
 heap_lang/lib/barrier/specification.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index 3a517ebae..08e45f569 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -9,7 +9,6 @@ Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}.
 
 Local Notation iProp := (iPropG heap_lang Σ).
 
-(* TODO: Maybe notation for LocV (and Loc)? *)
 Lemma barrier_spec (heapN N : namespace) :
   heapN ⊥ N →
   ∃ recv send : loc → iProp -n> iProp,
-- 
GitLab