From f96a894b14fe7095bb5ac5b937abd31e40316858 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 9 Sep 2017 16:30:21 +0200
Subject: [PATCH] Set notation scopes of some language stuff.

---
 theories/program_logic/ectx_language.v  |  8 ++++----
 theories/program_logic/ectxi_language.v | 10 ++++++----
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 1d337123b..69c5cc6a4 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 041a3bf56..71cb016b4 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.
-- 
GitLab