From 00db32d1f753892239e93ca55d9f5de4251e66af Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 3 May 2018 22:43:58 +0200
Subject: [PATCH] Don't create `<pers>` modalities in `iSplit`  when the BI is
 affine.

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

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 5b118cd10..1e6b32313 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -23,7 +23,7 @@ Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
 Global Instance into_absorbingly_absorbing P : Absorbing P → IntoAbsorbingly P P | 1.
 Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
 Global Instance into_absorbingly_intuitionistically P :
-  IntoAbsorbingly (<pers> P) (â–¡ P) | 0.
+  IntoAbsorbingly (<pers> P) (â–¡ P) | 2.
 Proof.
   by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
 Qed.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index b8024b8f8..19c61a492 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -460,4 +460,10 @@ Proof.
   - iDestruct "H" as "[_ [$ _]]".
   - iDestruct "H" as "[_ [_ #$]]".
 Qed.
+
+Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
+Proof.
+  iIntros "[??]". iSplit; last done.
+  lazymatch goal with |- coq_tactics.envs_entails _ (â–¡ P) => done end.
+Qed.
 End tests.
-- 
GitLab