From 51eea32e38cc4a7731585c151027fa31a10f9c7e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 Jul 2016 09:34:41 +0200
Subject: [PATCH] =?UTF-8?q?Make=20level=20of=20-n>=20the=20same=20as=20?=
 =?UTF-8?q?=E2=86=92.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 algebra/cofe.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index 826db7356..438b7652a 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -260,9 +260,10 @@ Section cofe_mor.
 End cofe_mor.
 
 Arguments cofe_mor : clear implicits.
-Infix "-n>" := cofe_mor (at level 45, right associativity).
-Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
-  Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
+Notation "A -n> B" :=
+  (cofe_mor A B) (at level 99, B at level 200, right associativity).
+Instance cofe_mor_inhabited {A B : cofeT} `{Inhabited B} :
+  Inhabited (A -n> B) := populate (λne _, inhabitant).
 
 (** Identity and composition and constant function *)
 Definition cid {A} : A -n> A := CofeMor id.
-- 
GitLab