diff --git a/heap_lang/notation.v b/heap_lang/notation.v index c92c12716a8397af257c77edf3325fe52c94e942..156222098423562f2c1f3386498819c6acebeac8 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)