diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 68cbb353f27cebf82bdf58fe3f160ba966eb527b..09b9314e3f70c1769e4a3e17cce7127860809325 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -23,7 +23,10 @@ Coercion of_val : val >-> expr.
    was needed, the coercion of_val will be called. The notations for literals
    are not put in any scope so as to avoid lots of annoying %L scopes while
    pretty printing. *)
+Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : lang_scope.
 Notation "' l" := (Lit l%Z) (at level 8, format "' l").
+Notation "'match:' e0 'with' x1 => e1 | x2 => e2 'end'" := (Case e0 x1 e1 x2 e2)
+  (e0, x1, e1, x2, e2 at level 200) : lang_scope.
 Notation "' l" := (LitV l%Z) (at level 8, format "' l").
 Notation "'()"  := (Lit LitUnit) (at level 0).
 Notation "'()"  := (LitV LitUnit) (at level 0).