From dcaf9240822974ac16047d71ecf93d1e6d0e975c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Jul 2016 13:28:29 +0200
Subject: [PATCH] =?UTF-8?q?Make=20=E2=88=96=20left=20associative.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index 86b1036f..f354f0e0 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -590,7 +590,7 @@ Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : C_scope.
 
 Class Difference A := difference: A → A → A.
 Instance: Params (@difference) 2.
-Infix "∖" := difference (at level 40) : C_scope.
+Infix "∖" := difference (at level 40, left associativity) : C_scope.
 Notation "(∖)" := difference (only parsing) : C_scope.
 Notation "( x ∖)" := (difference x) (only parsing) : C_scope.
 Notation "(∖ x )" := (λ y, difference y x) (only parsing) : C_scope.
-- 
GitLab