From 69fea45da754a7b77a7884bf1cec76fdca1201ff Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 5 Mar 2016 13:01:10 +0100
Subject: [PATCH] improve match notation printing

---
 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 c92c12716..156222098 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -37,7 +37,7 @@ Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
   (e0, x1, e1, x2, e2 at level 200) : expr_scope.
 Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
   (Match e0 x2 e2 x1 e1)
-  (e0, x1, e1, x2, e2 at level 200) : expr_scope.
+  (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
 Notation "()" := LitUnit : val_scope.
 Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
 Notation "'ref' e" := (Alloc e%E)
-- 
GitLab