diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index f0069a565293c13b5d0367924b4af840035ff226..4ffe8d1761388d6a285374f0881e3f9952a11c82 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -79,6 +79,10 @@ Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
   bupd_plainly (P : PROP) : (|==> ■ P) -∗ P.
 Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
 
+(** These rules for the interaction between the [â– ] and [|={E1,E2=>] modalities
+only make sense for affine logics. From the axioms below, one could derive
+[■ P ={E}=∗ P] (see the lemma [fupd_plainly_elim]), which in turn gives
+[True ={E}=∗ emp]. *)
 Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
   fupd_plainly_mask_empty E (P : PROP) :
     (|={E,∅}=> ■ P) ⊢ |={E}=> P;