From 3ef1bbb531bf3b43a8427f650ddf7891bf4852df Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 May 2018 11:58:44 +0200
Subject: [PATCH] =?UTF-8?q?Stronger=20`IntoWand`=20instance=20for=20the=20?=
 =?UTF-8?q?=E2=96=A1=20modality.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proofmode/class_instances_bi.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 84fbcaf6d..45e72fee4 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -419,8 +419,8 @@ Proof.
 Qed.
 
 Global Instance into_wand_intuitionistically p q R P Q :
-  IntoWand p q R P Q → IntoWand p q (□ R) P Q.
-Proof. by rewrite /IntoWand intuitionistically_elim. Qed.
+  IntoWand true q R P Q → IntoWand p q (□ R) P Q.
+Proof. rewrite /IntoWand /= => ->. by rewrite {1}intuitionistically_if_elim. Qed.
 Global Instance into_wand_persistently_true q R P Q :
   IntoWand true q R P Q → IntoWand true q (<pers> R) P Q.
 Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
-- 
GitLab