From 87e70e928900b8bec0cf067f5a79a3fb8d208912 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Feb 2016 00:54:02 +0100
Subject: [PATCH] =?UTF-8?q?The=20uPred=20connectives=20=E2=96=A0,=20?=
 =?UTF-8?q?=E2=96=A1=20and=20=E2=96=B7=20should=20be=20right=20associative?=
 =?UTF-8?q?.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 algebra/upred.v | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 64c01202f..3aa4b20bf 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -191,7 +191,8 @@ Arguments uPred_holds {_} _%I _ _.
 Arguments uPred_entails _ _%I _%I.
 Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
 Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
-Notation "■ φ" := (uPred_const φ%C%type) (at level 20) : uPred_scope.
+Notation "■ φ" := (uPred_const φ%C%type)
+  (at level 20, right associativity) : uPred_scope.
 Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
 Notation "'False'" := (uPred_const False) : uPred_scope.
 Notation "'True'" := (uPred_const True) : uPred_scope.
@@ -208,8 +209,10 @@ Notation "∀ x .. y , P" :=
   (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
 Notation "∃ x .. y , P" :=
   (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
-Notation "â–· P" := (uPred_later P) (at level 20) : uPred_scope.
-Notation "â–¡ P" := (uPred_always P) (at level 20) : uPred_scope.
+Notation "â–· P" := (uPred_later P)
+  (at level 20, right associativity) : uPred_scope.
+Notation "â–¡ P" := (uPred_always P)
+  (at level 20, right associativity) : uPred_scope.
 Infix "≡" := uPred_eq : uPred_scope.
 Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
 
-- 
GitLab