diff --git a/barrier/proof.v b/barrier/proof.v
index 47512b24a7cdf736d90b723433e4d32f95981219..4cbeeb322244ec8f2c7d7dcffe101ddc4df053d2 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.