From 0c5631c469d77be74f8bf7140ba706223dbe8bda Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Jan 2019 22:22:22 +0100
Subject: [PATCH] use WP sugar

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

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index f46b92465..65513253b 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -242,7 +242,7 @@ Lemma wp_wand_r s E e Φ Ψ :
   WP e @ s; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ s; E {{ Ψ }}.
 Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
 Lemma wp_frame_wand_l s E e Q Φ :
-  Q ∗ WP e @ s; E {{ λ v, Q -∗ Φ v }} -∗ WP e @ s; E {{ Φ }}.
+  Q ∗ WP e @ s; E {{ v, Q -∗ Φ v }} -∗ WP e @ s; E {{ Φ }}.
 Proof.
   iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
   iIntros (v) "HΦ". by iApply "HΦ".
-- 
GitLab