From e0d10c05fb04d4e138b4657c9103ffcfa357b2bd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Nov 2019 09:48:12 +0100
Subject: [PATCH] Properly set scopes for `ectx(i)_language`, like we do for
 `language`.

This fixes the problem in https://gitlab.mpi-sws.org/iris/iris/merge_requests/275#note_42062
---
 theories/program_logic/ectx_language.v  | 11 +++++++----
 theories/program_logic/ectxi_language.v | 12 +++++++-----
 2 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 5db8a54b9..4c8945ce8 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -61,13 +61,16 @@ Structure ectxLanguage := EctxLanguage {
     EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
 }.
 
+Bind Scope expr_scope with expr.
+Bind Scope val_scope with val.
+
 Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _ _} _.
-Arguments of_val {_} _%V.
-Arguments to_val {_} _%E.
+Arguments of_val {_} _.
+Arguments to_val {_} _.
 Arguments empty_ectx {_}.
 Arguments comp_ectx {_} _ _.
-Arguments fill {_} _ _%E.
-Arguments head_step {_} _%E _ _ _%E _ _.
+Arguments fill {_} _ _.
+Arguments head_step {_} _ _ _ _ _ _.
 
 (* From an ectx_language, we can construct a language. *)
 Section ectx_language.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 4b60cebbf..af769d0f0 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -65,11 +65,14 @@ Structure ectxiLanguage := EctxiLanguage {
     EctxiLanguageMixin of_val to_val fill_item head_step
 }.
 
+Bind Scope expr_scope with expr.
+Bind Scope val_scope with val.
+
 Arguments EctxiLanguage {_ _ _ _ _ _ _ _ _} _.
-Arguments of_val {_} _%V.
-Arguments to_val {_} _%E.
-Arguments fill_item {_} _ _%E.
-Arguments head_step {_} _%E _ _ _%E _ _.
+Arguments of_val {_} _.
+Arguments to_val {_} _.
+Arguments fill_item {_} _ _.
+Arguments head_step {_} _ _ _ _ _ _.
 
 Section ectxi_language.
   Context {Λ : ectxiLanguage}.
@@ -144,7 +147,6 @@ Section ectxi_language.
   Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
 End ectxi_language.
 
-Arguments fill {_} _ _%E.
 Arguments ectxi_lang_ectx : clear implicits.
 Arguments ectxi_lang : clear implicits.
 Coercion ectxi_lang_ectx : ectxiLanguage >-> ectxLanguage.
-- 
GitLab