From 3477ed5947595c0273461af513b23bb68e6a910a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 24 Feb 2016 15:09:29 +0100
Subject: [PATCH] re-add a TODO that has not been solved

---
 barrier/barrier.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index 7a2496182..9621bcdf4 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -180,7 +180,9 @@ Section proof.
     (∃ γ, barrier_ctx γ l P ★ sts_ownS γ low_states {[ Send ]})%I.
 
   Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
-  Proof. intros P1 P2 HP. rewrite /send. by setoid_rewrite HP. Qed.
+  Proof. (* TODO: This really ought to be doable by just calling a tactic.
+            It is just application of already registered congruence lemmas. *)
+    intros P1 P2 HP. rewrite /send. by setoid_rewrite HP. Qed.
  
   Definition recv (l : loc) (R : iProp) : iProp :=
     (∃ γ P Q i, barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★
-- 
GitLab