diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 27aad262710264e3546b1b36b158b588791386d9..4a64793a0cc79df75d0f6564b205ee2216d61097 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -117,6 +117,11 @@ Arguments bi_wandM {_} !_%I _%I /.
 Notation "mP -∗? Q" := (bi_wandM mP Q)
   (at level 99, Q at level 200, right associativity) : bi_scope.
 
+(** This class is required for the [iLöb] tactic. For most logics this class
+should not be inhabited directly, but the instance [Contractive (▷) → BiLöb PROP]
+in [derived_laws_sbi] should be used. A direct instance of the class is useful
+when considering a BI logic with a discrete OFE, instead of a OFE that takes
+step-indexing of the logic in account.*)
 Class BiLöb (PROP : bi) :=
   löb (P : PROP) : (▷ P → P) ⊢ P.
 Hint Mode BiLöb ! : typeclass_instances.