From 6d021c73e17b878fb5c951ed27ac703faaf4916f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Sep 2016 17:07:17 +0200
Subject: [PATCH] Put notations for proofmode environment manipulation into a
 module.

---
 proofmode/coq_tactics.v  |  8 +-------
 proofmode/environments.v | 17 ++++++++++-------
 2 files changed, 11 insertions(+), 14 deletions(-)

diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index e9f809ec2..2d8e234ac 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -3,13 +3,7 @@ From iris.algebra Require Import upred_big_op upred_tactics.
 From iris.proofmode Require Export environments classes.
 From iris.prelude Require Import stringmap hlist.
 Import uPred.
-
-Local Notation "Γ !! j" := (env_lookup j Γ).
-Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
-Local Notation "' ( x1 , x2 ) ← y ; z" :=
-  (match y with Some (x1,x2) => z | None => None end).
-Local Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
-  (match y with Some (x1,x2,x3) => z | None => None end).
+Import env_notations.
 
 Record envs (M : ucmraT) :=
   Envs { env_persistent : env (uPred M); env_spatial : env (uPred M) }.
diff --git a/proofmode/environments.v b/proofmode/environments.v
index e3385e5fd..a262ae95d 100644
--- a/proofmode/environments.v
+++ b/proofmode/environments.v
@@ -10,18 +10,21 @@ Arguments Esnoc {_} _ _%string _.
 Instance: Params (@Enil) 1.
 Instance: Params (@Esnoc) 1.
 
-Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
-Local Notation "' ( x1 , x2 ) ← y ; z" :=
-  (match y with Some (x1,x2) => z | None => None end).
-Local Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
-  (match y with Some (x1,x2,x3) => z | None => None end).
-
 Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
   match Γ with
   | Enil => None
   | Esnoc Γ j x => if decide (i = j) then Some x else env_lookup i Γ
   end.
-Local Notation "Γ !! j" := (env_lookup j Γ).
+
+Module env_notations.
+  Notation "x ← y ; z" := (match y with Some x => z | None => None end).
+  Notation "' ( x1 , x2 ) ← y ; z" :=
+    (match y with Some (x1,x2) => z | None => None end).
+  Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
+    (match y with Some (x1,x2,x3) => z | None => None end).
+  Notation "Γ !! j" := (env_lookup j Γ).
+End env_notations.
+Import env_notations.
 
 Inductive env_wf {A} : env A → Prop :=
   | Enil_wf : env_wf Enil
-- 
GitLab