From bf5df6e87d259c0e320ac5545cacb88b4744b509 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 10 Jun 2018 10:44:52 +0200
Subject: [PATCH] fix iSpecialize on pure assertions

---
 tests/proofmode.v                       | 4 ++++
 theories/proofmode/class_instances_bi.v | 7 ++++++-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 2d395c27e..3905f8bb7 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -111,6 +111,10 @@ Lemma test_iSpecialize_auto_frame P Q R :
   (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
 Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
 
+Lemma test_iSpecialize_pure (φ : Prop) Q R:
+  φ → (⌜φ⌝ -∗ Q) → Q.
+Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
+
 Lemma test_iSpecialize_Coq_entailment P Q R :
   P → (P -∗ Q) → Q.
 Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index ac035af93..cf4a2743c 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -806,8 +806,13 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
 Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
 Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
-Global Instance into_forall_wand P Q : IntoForall (P -∗ Q) (λ _ : bi_emp_valid P, Q).
+(* These instances must be used only after [into_forall_wand_pure] in
+[class_instances_sbi] failed. *)
+Global Instance into_forall_wand P Q : IntoForall (P -∗ Q) (λ _ : bi_emp_valid P, Q) | 10.
 Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite emp_wand //. Qed.
+Global Instance into_forall_impl `{!BiAffine PROP} P Q :
+  IntoForall (P → Q) (λ _ : bi_emp_valid P, Q) | 10.
+Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl //. Qed.
 
 (* FromForall *)
 Global Instance from_forall_forall {A} (Φ : A → PROP) :
-- 
GitLab