From 2ba9728f98573d4a63823e8d7b7422eb6d1d984e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 27 Feb 2016 02:12:58 +0100
Subject: [PATCH] Improve notation for Case.
---
heap_lang/notation.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 09b9314e3..ebdb983b9 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -25,7 +25,8 @@ Coercion of_val : val >-> expr.
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)
+Notation "'match:' e0 'with' 'injL' x1 => e1 | 'injR' 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).
--
GitLab