diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 80b628ae8f2e69bac86108ee2d2e6a235582b95a..fdeb3a982771514003b786b90575c8b3ae70b39d 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -134,7 +134,11 @@ Arguments löb_weak {_ _} _ _.
 Notation BiLaterContractive PROP :=
   (Contractive (bi_later (PROP:=PROP))) (only parsing).
 
-(* An instance of [BiPureForall] is derivable if we assume excluded middle in
-Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
+(** The class [BiPureForall] states that universal quantification commutes with
+the embedding of pure propositions. The reverse direction of the entailment
+described by this type class is derivable, so it is not included.
+
+An instance of [BiPureForall] itself is derivable if we assume excluded middle
+in Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
 Class BiPureForall (PROP : bi) :=
   pure_forall_2 : ∀ {A} (φ : A → Prop), (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.