From 377c2d147f5fdbc14b5ebc9b0d4163765218ae09 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Oct 2020 13:52:16 +0200
Subject: [PATCH] More Coqdoc.

---
 theories/bi/derived_connectives.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 80b628ae8..fdeb3a982 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 ⌝.
-- 
GitLab