More Coqdoc.

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 ⌝.