diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index e4e5dc55ab18da8a7d11477327a42b06b01f6ebb..31b9b4c7f8f216db8c7157fceaba828c16c3e4b2 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -531,11 +531,12 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
 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 Lam x e := (Rec BAnon x e) (only parsing).
+Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
+Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
+Notation LamV x e := (RecV BAnon x e) (only parsing).
+Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
+Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
+Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
+
 Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
-Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).