From e46a7529bb22bcba4c7756f1cbecb51b6d85dd2d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Sep 2016 16:07:08 +0200
Subject: [PATCH] Introduce notation excl' (like Excl' and ExclNone').

---
 algebra/auth.v | 4 ++--
 algebra/excl.v | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/algebra/auth.v b/algebra/auth.v
index 7d04ae801..5e7a7633c 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import upred updates.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
-Record auth (A : Type) := Auth { authoritative : option (excl A); auth_own : A }.
+Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
 Add Printing Constructor auth.
 Arguments Auth {_} _ _.
 Arguments authoritative {_} _.
@@ -14,7 +14,7 @@ Notation "● a" := (Auth (Excl' a) ∅) (at level 20).
 (* COFE *)
 Section cofe.
 Context {A : cofeT}.
-Implicit Types a : option (excl A).
+Implicit Types a : excl' A.
 Implicit Types b : A.
 Implicit Types x y : auth A.
 
diff --git a/algebra/excl.v b/algebra/excl.v
index 63c884b67..f93c4339a 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -9,6 +9,7 @@ Inductive excl (A : Type) :=
 Arguments Excl {_} _.
 Arguments ExclBot {_}.
 
+Notation excl' A := (option (excl A)).
 Notation Excl' x := (Some (Excl x)).
 Notation ExclBot' := (Some ExclBot).
 
-- 
GitLab