From 2e4bd8f55acf0686f745d56e97e7b50ef4725207 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 20 Mar 2020 13:19:56 +0100
Subject: [PATCH] =?UTF-8?q?Instance=20for=20`Affine=20(=E2=96=A1=3Fp=20P)`?=
 =?UTF-8?q?.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/derived_laws_bi.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 8ce55d3ab..724ffb34a 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -1398,6 +1398,8 @@ Global Instance affinely_if_affine p P : Affine P → Affine (<affine>?p P).
 Proof. destruct p; simpl; apply _. Qed.
 Global Instance intuitionistically_affine P : Affine (â–¡ P).
 Proof. rewrite /bi_intuitionistically. apply _. Qed.
+Global Instance intuitionistically_if_affine p P : Affine P → Affine (□?p P).
+Proof. destruct p; simpl; apply _. Qed.
 
 (* Absorbing instances *)
 Global Instance pure_absorbing φ : Absorbing (PROP:=PROP) ⌜φ⌝.
-- 
GitLab