From 784353e0b95df261b500ff8a2dd1f67c3c0ae8c7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 Apr 2018 19:32:26 +0200
Subject: [PATCH] improve wp_apply evar test

---
 theories/tests/heap_lang.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 0d6d2c8d9..1e71aaba0 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -105,9 +105,9 @@ Section LiftingTests.
     WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }]%I.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 
-  Lemma wp_apply_evar e :
-    (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
-  Proof. iIntros "H". wp_apply "H". done. Qed.
+  Lemma wp_apply_evar e P :
+    P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
+  Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
 
 End LiftingTests.
 
-- 
GitLab