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

---
 theories/utils/switch.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/utils/switch.v b/theories/utils/switch.v
index 4e4c602..e44f234 100644
--- a/theories/utils/switch.v
+++ b/theories/utils/switch.v
@@ -54,7 +54,7 @@ Qed.
 Lemma switch_lams_spec `{heapGS Σ} y i n ws vs e Φ :
   length vs = n →
   WP subst_map (map_string_seq y i vs ∪ ws) e {{ Φ }} -∗
-  WP subst_map ws (switch_lams y i n e) {{ w, WP fill (AppLCtx <$> vs) (w : val) {{ Φ }} }}.
+  WP subst_map ws (switch_lams y i n e) {{ w, WP fill (AppLCtx <$> vs) (of_val w) {{ Φ }} }}.
   (* 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 [w] binder here. *)
 Proof.
-- 
GitLab