diff --git a/heap_lang/notation.v b/heap_lang/notation.v index 4325f3f4a76e51287a9cff454fa3697c8330c9e0..fc50c809563d756f6d9fbffb752eeb63eda5b62c 100644 --- a/heap_lang/notation.v +++ b/heap_lang/notation.v @@ -20,9 +20,11 @@ Coercion of_val : val >-> expr. (* What about Arguments for hoare triples?. *) Notation "' l" := (Lit l) (at level 8, format "' l") : lang_scope. Notation "' l" := (LitV l) (at level 8, format "' l") : lang_scope. -Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope. -Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope. -Notation "- e" := (UnOp MinusUnOp e%L) (at level 35, right associativity) : lang_scope. +Notation "! e" := (Load e%L) (at level 10, right associativity) : lang_scope. +Notation "'ref' e" := (Alloc e%L) + (at level 30, right associativity) : lang_scope. +Notation "- e" := (UnOp MinusUnOp e%L) + (at level 35, right associativity) : lang_scope. Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L) (at level 50, left associativity) : lang_scope. Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L)