diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 1d337123b64cc3ba277d1d25d0bf20f691c98dcf..69c5cc6a41ffb3fefc71b2381357f7682abb9956 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -36,12 +36,12 @@ Class EctxLanguage (expr val ectx state : Type) := {
     exists K'', K' = comp_ectx K K'';
 }.
 
-Arguments of_val {_ _ _ _ _} _.
-Arguments to_val {_ _ _ _ _} _.
+Arguments of_val {_ _ _ _ _} _%V.
+Arguments to_val {_ _ _ _ _} _%E.
 Arguments empty_ectx {_ _ _ _ _}.
 Arguments comp_ectx {_ _ _ _ _} _ _.
-Arguments fill {_ _ _ _ _} _ _.
-Arguments head_step {_ _ _ _ _} _ _ _ _ _.
+Arguments fill {_ _ _ _ _} _ _%E.
+Arguments head_step {_ _ _ _ _} _%E _ _%E _ _.
 
 Arguments to_of_val {_ _ _ _ _} _.
 Arguments of_to_val {_ _ _ _ _} _ _ _.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 041a3bf561fd3342cc8ba849c9b935bc8133b23e..71cb016b4c3a9f891fd55722c8ed149a8c784dd6 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -26,10 +26,10 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
     head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e);
 }.
 
-Arguments of_val {_ _ _ _ _} _.
-Arguments to_val {_ _ _ _ _} _.
-Arguments fill_item {_ _ _ _ _} _ _.
-Arguments head_step {_ _ _ _ _} _ _ _ _ _.
+Arguments of_val {_ _ _ _ _} _%V.
+Arguments to_val {_ _ _ _ _} _%E.
+Arguments fill_item {_ _ _ _ _} _ _%E.
+Arguments head_step {_ _ _ _ _} _%E _ _%E _ _.
 
 Arguments to_of_val {_ _ _ _ _} _.
 Arguments of_to_val {_ _ _ _ _} _ _ _.
@@ -101,3 +101,5 @@ Section ectxi_language.
     LanguageCtx (ectx_lang expr) (fill_item Ki).
   Proof. change (LanguageCtx _ (fill [Ki])). apply _. Qed.
 End ectxi_language.
+
+Arguments fill {_ _ _ _ _} _ _%E.