fix tests

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 :
@@ -315,14 +315,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.

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.

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.