From 4fe52b0b4a85c0e69ac593fa06168804080a7420 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 May 2023 13:06:16 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 iris/bi/plainly.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 06b1ada1e..b55cbb110 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -134,7 +134,7 @@ Section plainly_derived.
     Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
   Proof. intros P Q; apply plainly_mono. Qed.
 
-  (* Not an instance, see the bottom of this file *)
+  (* Not an instance; registered as [Hint Immediate] at the bottom of this file *)
   Lemma plain_persistent P : Plain P → Persistent P.
   Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
 
-- 
GitLab