From b2b558ac9e8b7d43e9e6e21a61dda3a19c1b62b2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 7 Aug 2020 15:53:33 +0200
Subject: [PATCH] add top-level coqdoc comment to excl_auth

---
 theories/algebra/lib/excl_auth.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/algebra/lib/excl_auth.v b/theories/algebra/lib/excl_auth.v
index 5358d8dc1..baed9dd5b 100644
--- 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 :=
-- 
GitLab