From c9760db373d0dbf233ccda0f375cb611155d7c8c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Oct 2018 08:58:05 +0200
Subject: [PATCH] Comment about BiFUpdPlainly and affine BIs.

---
 theories/bi/updates.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index f0069a565..4ffe8d176 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -79,6 +79,10 @@ Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
   bupd_plainly (P : PROP) : (|==> ■ P) -∗ P.
 Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
 
+(** These rules for the interaction between the [â– ] and [|={E1,E2=>] modalities
+only make sense for affine logics. From the axioms below, one could derive
+[■ P ={E}=∗ P] (see the lemma [fupd_plainly_elim]), which in turn gives
+[True ={E}=∗ emp]. *)
 Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
   fupd_plainly_mask_empty E (P : PROP) :
     (|={E,∅}=> ■ P) ⊢ |={E}=> P;
-- 
GitLab