From c52b1300bb7ca48d72f810f82e2348e8b62650dd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 1 Mar 2021 19:21:57 +0100
Subject: [PATCH] comment on iAaccIntro

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

diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index c75b517ac..7bd8fa78f 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -453,7 +453,7 @@ Section proof_mode.
   Qed.
 End proof_mode.
 
-(** Now the coq-level tactics *)
+(** * Now the coq-level tactics *)
 
 Tactic Notation "iAuIntro" :=
   iStartProof; eapply tac_aupd_intro; [
@@ -461,6 +461,10 @@ Tactic Notation "iAuIntro" :=
   | iSolveTC || fail "iAuIntro: not all spatial assumptions are laterable"
   | (* P = ...: make the P pretty *) pm_reflexivity
   | (* the new proof mode goal *) ].
+
+(** Tactic to apply [aacc_intro]. This only really works well when you have
+[α ?] already and pass it as [iAaccIntro with "Hα"]. Doing
+[rewrite /atomic_acc /=] is an entirely legitimate alternative. *)
 Tactic Notation "iAaccIntro" "with" constr(sel) :=
   iStartProof; lazymatch goal with
   | |- environments.envs_entails _ (@atomic_acc ?PROP ?H ?TA ?TB ?Eo ?Ei ?α ?P ?β ?Φ) =>
-- 
GitLab