diff --git a/tests/one_shot.v b/tests/one_shot.v
index 248a387c9b442364e7797c0e3a8b5d3726236016..12ac80df3a2df7ad270200c821b1f777016a15dd 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -46,7 +46,7 @@ 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 : val) #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+    □ WP f2 #() {{ g, □ WP (of_val g) #() {{ _, 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 #() {{ Φ }}.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 28ac413f5c8cb281783fcdbd11b3b6a85c029480..5a23af9f5332fb45b30bdc334aabf9fb1b54f90c 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -60,7 +60,7 @@ 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 : val) #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+    □ WP f2 #() {{ g, □ WP (of_val g) #() {{ _, 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 #() {{ Φ }}.