From 98d7ce9bbbc8ed463b0cb5289dc9f00f831ee985 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Jul 2016 11:14:55 +0200
Subject: [PATCH] Fix the match notation in heap_lang for option.

---
 heap_lang/notation.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 9747dfcdd..05e173432 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.
-- 
GitLab