diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 5db8a54b9b98b1ba412134b8f27414136b51603e..4c8945ce8308005960e5ebf6c882fe2e94b985ce 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 4b60cebbfa6342df5820f5c9d262d9e3eed1d9ea..af769d0f0a9177549d99484ad55c663a991f999b 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.