diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index e9f809ec263f82d8c59803f58f83e561fbac4ba6..2d8e234ac739ca9cf6383db51610a557158ba371 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 e3385e5fdd9e8ec8b9d92bcbccbce153fbd03bcd..a262ae95d181732d34f5a9ae14a132ca1efa0a2d 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