From 59999b0f9e399cca56deac534e533dc17897661e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 23 Nov 2017 12:20:47 +0100
Subject: [PATCH] Make language argument of `LanguageCtx` implicit.

It can be infered now.
---
 theories/program_logic/ectx_language.v  | 2 +-
 theories/program_logic/ectxi_language.v | 4 ++--
 theories/program_logic/language.v       | 4 ++--
 theories/program_logic/weakestpre.v     | 4 ++--
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 40ea10294..9578d5785 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -176,7 +176,7 @@ Section ectx_language.
   Qed.
 
   (* Every evaluation context is a context. *)
-  Global Instance ectx_lang_ctx K : LanguageCtx _ (fill K).
+  Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
   Proof.
     split; simpl.
     - eauto using fill_not_val.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 6c0f58131..c622cd164 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -114,8 +114,8 @@ Section ectxi_language.
     intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
   Qed.
 
-  Global Instance ectxi_lang_ctx_item Ki : LanguageCtx _ (fill_item Ki).
-  Proof. change (LanguageCtx ectxi_lang (fill [Ki])). apply _. Qed.
+  Global Instance ectxi_lang_ctx_item Ki : LanguageCtx (fill_item Ki).
+  Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
 End ectxi_language.
 
 Arguments fill {_} _ _%E.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 6b1a9770c..660965699 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -39,7 +39,7 @@ Canonical Structure exprC Λ := leibnizC (expr Λ).
 
 Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
 
-Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
+Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
   fill_not_val e :
     to_val e = None → to_val (K e) = None;
   fill_step e1 σ1 e2 σ2 efs :
@@ -50,7 +50,7 @@ Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
     ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 efs
 }.
 
-Instance language_ctx_id Λ : LanguageCtx Λ id.
+Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
 Proof. constructor; naive_solver. Qed.
 
 Section language.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 7d63d87bb..97096107c 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -174,7 +174,7 @@ Proof.
   iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
 Qed.
 
-Lemma wp_bind K `{!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.
@@ -189,7 +189,7 @@ Proof.
   by iApply "IH".
 Qed.
 
-Lemma wp_bind_inv K `{!LanguageCtx Λ K} E e Φ :
+Lemma wp_bind_inv K `{!LanguageCtx K} E e Φ :
   WP K e @ E {{ Φ }} ⊢ WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
-- 
GitLab