diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 2d3f5047040fe1b1ba3651d108297dbcf74d6d77..bcc2e47de76d4dda4bc91f7f2a6486b82dd67364 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,8 +1,7 @@
-(** This file is essentially a bunch of testcases. *)
 From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import adequacy.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import lang adequacy proofmode notation.
+(* Import lang *again*. This used to break notation. *)
+From iris.heap_lang Require Import lang.
 Set Default Proof Using "Type".
 
 Section tests.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index e4e5dc55ab18da8a7d11477327a42b06b01f6ebb..aea432737f54739cbea2befcc37eae55983e9ea8 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -529,13 +529,3 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
 
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.
-
-(** Define some derived forms *)
-Notation Lam x e := (Rec BAnon x e).
-Notation Let x e1 e2 := (App (Lam x e2) e1).
-Notation Seq e1 e2 := (Let BAnon e1 e2).
-Notation LamV x e := (RecV BAnon x e).
-Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
-Notation SeqCtx e2 := (LetCtx BAnon e2).
-Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
-Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 3751417fa10d2a6f30996a34389d880a86993bcb..340f784071a2f84a4f4b139de84903958d7de79d 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -2,6 +2,17 @@ From iris.program_logic Require Import language.
 From iris.heap_lang Require Export lang tactics.
 Set Default Proof Using "Type".
 
+(** Define some derived forms. Happens in the same file because the order of
+    this and the following notations being defined is very relevant. *)
+Notation Lam x e := (Rec BAnon x e).
+Notation Let x e1 e2 := (App (Lam x e2) e1).
+Notation Seq e1 e2 := (Let BAnon e1 e2).
+Notation LamV x e := (RecV BAnon x e).
+Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
+Notation SeqCtx e2 := (LetCtx BAnon e2).
+Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
+Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
+
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 7481a1a6d3874b4d2ea81bf0c22681d1999bf87d..7631e8a85b63bc9ee4996e5fb2112e0a780d4caf 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -2,6 +2,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics lifting.
+From iris.heap_lang Require Import notation.
 Set Default Proof Using "Type".
 Import uPred.