diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 9747dfcdd0a6078608f499d54b665454b57c5e9d..05e173432ec7b604ec1ba7fbc5f8a765c6edd02b 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -114,6 +114,6 @@ Notation SOMEV x := (InjRV x).
 Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200) : expr_scope.
-Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 |  'end'" :=
+Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.