From 4e43a2706e0239e468a3408b44e82b09914556d7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Feb 2016 20:17:00 +0100
Subject: [PATCH] comment on the validity trick in auth

---
 program_logic/auth.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/program_logic/auth.v b/program_logic/auth.v
index c929c8fbe..54e802a23 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -8,6 +8,8 @@ Class AuthInG Λ Σ (i : gid) (A : cmraT) `{Empty A} := {
   auth_timeless (a : A) :> Timeless a;
 }.
 
+(* TODO: Once we switched to RAs, it is no longer necessary to remember that a is
+   constantly valid. *)
 Definition auth_inv {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
   (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ := (∃ a, (■✓a ∧ own i γ (● a)) ★ φ a)%I.
 Definition auth_own {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
-- 
GitLab