From 53b2097438351ca9c9ed6cfece976e2a743859be Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Jun 2022 11:15:26 -0700
Subject: [PATCH] docs for aupd_intro

---
 iris/bi/lib/atomic.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 2ae6b8157..b9eac03ef 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -273,6 +273,8 @@ Section lemmas.
     apply _.
   Qed.
 
+  (** The introduction lemma for atomic_update. This should usually not be used
+  directly; use the [iAuIntro] tactic instead. *)
   Lemma aupd_intro P Q α β Eo Ei Φ :
     Absorbing P → Persistent P → Laterable Q →
     (P ∧ Q -∗ atomic_acc Eo Ei α Q β Φ) →
-- 
GitLab