diff --git a/algebra/cofe.v b/algebra/cofe.v index 826db73562ec90fe213ce57cf59d628019473621..438b7652a02f5f0342677b765330eccbe79471d0 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.