From 457c12fea1d5ef3a2df17fd9368d8c89a9287e18 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 9 Dec 2016 13:35:51 +0100
Subject: [PATCH] Make some overlapping heap_lang notations parsing only.

---
 heap_lang/notation.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 9406c5c0c..58ca9a1b2 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -91,15 +91,15 @@ Notation "e1 || e2" :=
   (If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
 
 (** Notations for option *)
-Notation NONE := (InjL #()).
-Notation SOME x := (InjR x).
+Notation NONE := (InjL #()) (only parsing).
+Notation SOME x := (InjR x) (only parsing).
 
-Notation NONEV := (InjLV #()).
-Notation SOMEV x := (InjRV x).
+Notation NONEV := (InjLV #()) (only parsing).
+Notation SOMEV x := (InjRV x) (only parsing).
 
 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.
+  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
 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