diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 06b1ada1ee22a9eda4ba217bd5fb9cb6c775e9d0..b55cbb110568f0bd452ec0a25b8aa5c96260b1a5 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.