From efd172019b9dabd746c6007d61356202a1cc43c8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 May 2018 17:44:18 +0200
Subject: [PATCH] elim_inv_acc_with_close: also support ElimModal with a
 side-condition

---
 theories/proofmode/class_instances_bi.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index cc5092b6f..463eceb4d 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -868,15 +868,16 @@ Proof.
 Qed.
 
 Global Instance elim_inv_acc_with_close {X : Type}
-       φ Pinv Pin
+       φ1 φ2 Pinv Pin
        M1 M2 α β mγ Q Q' :
-  IntoAcc Pinv φ Pin M1 M2 α β mγ →
-  (∀ R, ElimModal True false false (M1 R) R Q Q') →
-  ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x -∗ M2 (proofmode.base.from_option id emp (mγ x))))%I
+  IntoAcc Pinv φ1 Pin M1 M2 α β mγ →
+  (∀ R, ElimModal φ2 false false (M1 R) R Q Q') →
+  ElimInv (X:=X) (φ1 ∧ φ2) Pinv Pin
+          α (Some (λ x, β x -∗ M2 (proofmode.base.from_option id emp (mγ x))))%I
           Q (λ _, Q').
 Proof.
   rewrite /ElimAcc /IntoAcc /ElimInv.
-  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
+  iIntros (Hacc Helim [??]) "(Hinv & Hin & Hcont)".
   iMod (Hacc with "Hinv Hin") as (x) "[Hα Hclose]"; first done.
   iApply "Hcont". simpl. iSplitL "Hα"; done.
 Qed.
-- 
GitLab