From 25131c0296d70ad5090c577472d443c97d743220 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 31 Oct 2022 07:58:25 +0100
Subject: [PATCH] =?UTF-8?q?Better=20instance=20for=20`IntoWand`=20of=20`?=
 =?UTF-8?q?=E2=88=80=20=5F=20:=20=CF=86,=20P`.=20Fixes=20#799.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/proofmode/class_instances.v | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index dc207ad91..205798085 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -497,11 +497,13 @@ Proof.
           -impl_wand_intuitionistically -pure_impl_forall
           bi.persistently_elim //.
 Qed.
-Global Instance into_wand_forall_prop_false p (φ : Prop) P :
-  Absorbing P → IntoWand p false (∀ _ : φ, P) ⌜ φ ⌝ P.
+Global Instance into_wand_forall_prop_false p (φ : Prop) Pφ P :
+  MakeAffinely ⌜ φ ⌝ Pφ →
+  IntoWand p false (∀ _ : φ, P) Pφ P.
 Proof.
-  intros ?.
-  rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //.
+  rewrite /MakeAffinely /IntoWand=> <-.
+  rewrite (intuitionistically_if_elim p) /=.
+  by rewrite -pure_impl_forall -persistent_impl_wand_affinely.
 Qed.
 
 Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
-- 
GitLab