From 7ee261cf8a5d497748cd731dd3158dae86a73fcc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 3 May 2021 12:21:49 +0200
Subject: [PATCH] use wp_frame_wand where suitable

---
 iris/program_logic/atomic.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 04a07d03e..63f075cbc 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -112,7 +112,7 @@ Section lemmas.
     ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
   Proof.
     rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
-    iApply wp_frame_wand_l. iSplitL "HΦ"; first iAccu. iApply "Hwp".
+    iApply (wp_frame_wand with "HΦ"). iApply "Hwp".
     iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
     (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
     rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
-- 
GitLab