From aec84909bab9b4eec5340143497ff43101393161 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 25 Oct 2016 11:25:01 +0200
Subject: [PATCH] Make argument K of wp_bind explicit.

---
 program_logic/weakestpre.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index fc1e4de7e..9890456f7 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -145,7 +145,7 @@ Proof.
   iVs "HR". iVsIntro. iApply (wp_strong_mono E2 _ _ Φ); try iFrame; eauto.
 Qed.
 
-Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
+Lemma wp_bind K `{!LanguageCtx Λ K} E e Φ :
   WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
-- 
GitLab