From 3db59fe2945fee36fc307423701f170846773ced Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Mar 2021 14:14:41 +0100
Subject: [PATCH] fix tests

---
 tests/heap_lang.v     | 12 ++++++------
 tests/one_shot.v      |  4 +++-
 tests/one_shot_once.v |  4 +++-
 3 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index a05b855a2..56ccc8c66 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -176,9 +176,9 @@ Section tests.
   Proof. Fail wp_store. Abort.
 
   Check "(t)wp_bind_fail".
-  Lemma wp_bind_fail : ⊢ WP #() {{ v, True }}.
+  Lemma wp_bind_fail : ⊢ WP (of_val #()) {{ v, True }}.
   Proof. Fail wp_bind (!_)%E. Abort.
-  Lemma twp_bind_fail : ⊢ WP #() [{ v, True }].
+  Lemma twp_bind_fail : ⊢ WP (of_val #()) [{ v, True }].
   Proof. Fail wp_bind (!_)%E. Abort.
 
   Lemma wp_apply_evar e P :
@@ -186,10 +186,10 @@ Section tests.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
 
   Lemma wp_pures_val (b : bool) :
-    ⊢ WP #b {{ _, True }}.
+    ⊢ WP (of_val #b) {{ _, True }}.
   Proof. wp_pures. done. Qed.
   Lemma twp_pures_val (b : bool) :
-    ⊢ WP #b [{ _, True }].
+    ⊢ WP (of_val #b) [{ _, True }].
   Proof. wp_pures. done. Qed.
 
   Lemma wp_cmpxchg l v :
@@ -284,14 +284,14 @@ Section tests.
 
   Check "test_wp_finish_fupd".
   Lemma test_wp_finish_fupd (v : val) :
-    ⊢ WP v {{ v, |={⊤}=> True }}.
+    ⊢ WP of_val v {{ v, |={⊤}=> True }}.
   Proof.
     wp_pures. Show. (* No second fupd was added. *)
   Abort.
 
   Check "test_twp_finish_fupd".
   Lemma test_twp_finish_fupd (v : val) :
-    ⊢ WP v [{ v, |={⊤}=> True }].
+    ⊢ WP of_val v [{ v, |={⊤}=> True }].
   Proof.
     wp_pures. Show. (* No second fupd was added. *)
   Abort.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 0f93ccabf..1baad3075 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -46,7 +46,9 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
 Lemma wp_one_shot (Φ : val → iProp Σ) :
   (∀ f1 f2 : val,
     (∀ n : Z, □ WP f1 #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
-    □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+    □ WP f2 #() {{ g, □ WP (g : val) #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+      (* FIXME: Once we depend on Coq 8.13, make WP notation use [v closed binder]
+         so that we can add a type annotation at the [g] binder here. *)
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "Hf /=". pose proof (nroot .@ "N") as N.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 4b858ca73..022dc76ea 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -60,7 +60,9 @@ Qed.
 Lemma wp_one_shot (Φ : val → iProp Σ) :
   (∀ (f1 f2 : val) (T : iProp Σ), T ∗
     □ (∀ n : Z, T -∗ WP f1 #n {{ w, True }}) ∗
-    □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+    □ WP f2 #() {{ g, □ WP (g : val) #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+      (* FIXME: Once we depend on Coq 8.13, make WP notation use [v closed binder]
+         so that we can add a type annotation at the [g] binder here. *)
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "Hf /=". pose proof (nroot .@ "N") as N.
-- 
GitLab