diff --git a/algebra/auth.v b/algebra/auth.v
index 7d04ae801c93cb5a38f1e18e61e1980a117cb7ae..5e7a7633c7344a2dc87b44fe15e16653ef71d776 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 63c884b67a0ac2a91d301fae0cb2e87128908f14..f93c4339abcffeaf3eee3229d60b620b0d5be1ec 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).