From abfe86722e2ceca417321287cdf051cadacefeca Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Jun 2021 12:57:35 +0200
Subject: [PATCH] explicit coercion > type ascription

---
 tests/one_shot.v      | 2 +-
 tests/one_shot_once.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/one_shot.v b/tests/one_shot.v
index 248a387c9..12ac80df3 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 28ac413f5..5a23af9f5 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 #() {{ Φ }}.
-- 
GitLab