From ee8b3ce813169818b65e26286268488a1b4de8ce Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Dec 2015 15:33:15 +0100
Subject: [PATCH] Notation for auth that does not conflict with composition of
 functions.

---
 iris/auth.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris/auth.v b/iris/auth.v
index 66339bf20..cc51e16ff 100644
--- a/iris/auth.v
+++ b/iris/auth.v
@@ -6,8 +6,8 @@ Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
 Arguments Auth {_} _ _.
 Arguments authoritative {_} _.
 Arguments own {_} _.
-Notation "∘ x" := (Auth ExclUnit x) (at level 20).
-Notation "∙ x" := (Auth (Excl x) ∅) (at level 20).
+Notation "â—¯ x" := (Auth ExclUnit x) (at level 20).
+Notation "● x" := (Auth (Excl x) ∅) (at level 20).
 
 (* COFE *)
 Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
@@ -122,7 +122,7 @@ Proof.
   split; [apply (ra_empty_valid (A:=A))|].
   by intros x; constructor; simpl; rewrite (left_id _ _).
 Qed.
-Lemma auth_frag_op `{CMRA A} a b : ∘(a ⋅ b) ≡ ∘a ⋅ ∘b.
+Lemma auth_frag_op `{CMRA A} a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
 
 (* Functor *)
-- 
GitLab