From cb9adddc93441812593127508e83824dfb2d690d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 25 Feb 2016 09:34:45 +0100
Subject: [PATCH] bring back a TODO (again?)

---
 barrier/proof.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/barrier/proof.v b/barrier/proof.v
index 47512b24a..4cbeeb322 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -52,7 +52,7 @@ Definition recv (l : loc) (R : iProp) : iProp :=
     saved_prop_own i Q ★ ▷ (Q -★ R))%I.
 
 (** Setoids *)
-(* These lemmas really ought to be doable by just calling a tactic.
+(* TODO: These lemmas really ought to be doable by just calling a tactic.
    It is just application of already registered congruence lemmas. *)
 Global Instance waiting_ne n : Proper (dist n ==> (=) ==> dist n) waiting.
 Proof. intros P P' HP I ? <-. rewrite /waiting. by setoid_rewrite HP. Qed.
-- 
GitLab