From 81ba0b8bce37d53d6d7730e0e3c5abeb38e570ea Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 13 May 2018 21:35:26 +0200
Subject: [PATCH] False is affine.

---
 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 954707291..2eba05374 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -1274,6 +1274,8 @@ End persistent_bi_absorbing.
 (* Affine instances *)
 Global Instance emp_affine_l : Affine (PROP:=PROP) emp.
 Proof. by rewrite /Affine. Qed.
+Global Instance False_affine : Affine (PROP:=PROP) False.
+Proof. by rewrite /Affine False_elim. Qed.
 Global Instance and_affine_l P Q : Affine P → Affine (P ∧ Q).
 Proof. rewrite /Affine=> ->; auto. Qed.
 Global Instance and_affine_r P Q : Affine Q → Affine (P ∧ Q).
-- 
GitLab