From 3761273c9487cc4d1f159f61abf262354ef43849 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Feb 2016 09:09:16 +0100
Subject: [PATCH] auth: more precise comments

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

diff --git a/program_logic/auth.v b/program_logic/auth.v
index 3fbeeb7cc..c698c33a3 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -2,16 +2,17 @@ From algebra Require Export auth.
 From program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
-(* TODO: Once we switched to RAs, it is no longer necessary to remember that a
-is constantly valid. *)
 Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
   auth_inG :> inG Λ Σ (authRA A);
   auth_identity :> CMRAIdentity A;
+  (* TODO: Once we switched to RAs, this can be removed. *)
   auth_timeless (a : A) :> Timeless a;
 }.
 
 Section definitions.
   Context `{authG Λ Σ A} (γ : gname).
+  (* TODO: Once we switched to RAs, it is no longer necessary to remember that a
+     is constantly valid. *)
   Definition auth_inv (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
     (∃ a, (■ ✓ a ∧ own γ (● a)) ★ φ a)%I.
   Definition auth_own (a : A) : iPropG Λ Σ := own γ (◯ a).
-- 
GitLab