From abbe9f565cc8eb04b6f352088dc9545cdcada401 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 May 2020 15:07:13 +0200
Subject: [PATCH] =?UTF-8?q?Comment=20about=20`BiL=C3=B6b`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/derived_connectives.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 27aad2627..4a64793a0 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.
-- 
GitLab