From ee8c48750648240aece5c62761d5e382ce1e67d1 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 12 Feb 2016 00:55:08 +0100 Subject: [PATCH] Right associativity of some heap_lang constructs. --- heap_lang/notation.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/heap_lang/notation.v b/heap_lang/notation.v index 4325f3f4a..fc50c8095 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) -- GitLab