add top-level coqdoc comment to excl_auth

b2b558ac · Ralf Jung · 0e837bfd · b2b558ac
Commit b2b558ac authored Aug 07, 2020 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

theories/algebra/lib/excl_auth.v theories/algebra/lib/excl_auth.v +4 -0

No files found.
--- a/theories/algebra/lib/excl_auth.v
+++ b/theories/algebra/lib/excl_auth.v
@@ -2,6 +2,10 @@ From iris.algebra Require Export auth excl updates.
 From iris.algebra Require Import local_updates.
 From iris.base_logic Require Import base_logic.

+(** Authoritative CMRA where the fragment is exclusively owned.
+This is effectively a single "ghost variable" with two views, the frament [◯E a]
+and the authority [●E a]. *)
+
 Definition excl_authR (A : ofeT) : cmraT :=
  authR (optionUR (exclR A)).
 Definition excl_authUR (A : ofeT) : ucmraT :=