From 5b36e201c45f928132b38e5c14f4b35e6116b883 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Feb 2016 03:06:18 +0100
Subject: [PATCH] More general and Global version of auth_timeless.

---
 algebra/auth.v       | 6 +++---
 program_logic/auth.v | 8 --------
 2 files changed, 3 insertions(+), 11 deletions(-)

diff --git a/algebra/auth.v b/algebra/auth.v
index d21944475..c64086068 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -50,8 +50,8 @@ Proof.
     apply (conv_compl (chain_map own c) n).
 Qed.
 Canonical Structure authC := CofeT auth_cofe_mixin.
-Instance Auth_timeless (ea : excl A) (b : A) :
-  Timeless ea → Timeless b → Timeless (Auth ea b).
+Global Instance auth_timeless (x : auth A) :
+  Timeless (authoritative x) → Timeless (own x) → Timeless x.
 Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
 Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
 Proof. by intros ? [??] [??] [??]; f_equal'; apply leibniz_equiv. Qed.
@@ -140,7 +140,7 @@ Proof.
   split; simpl.
   * by apply (@cmra_empty_valid A _).
   * by intros x; constructor; rewrite /= left_id.
-  * apply Auth_timeless; apply _.
+  * apply _.
 Qed.
 Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index a063d70d8..afffd9862 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -11,14 +11,6 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types γ : gname.
 
-  (* Adding this locally only, since it overlaps with Auth_timelss in algebra/auth.v.
-     TODO: Would moving this to auth.v and making it global break things? *)
-  Local Instance AuthA_timeless (x : auth A) : Timeless x.
-  Proof.
-    (* FIXME: "destruct x; auto with typeclass_instances" should find this through Auth, right? *)
-    destruct x. apply Auth_timeless; apply _.
-  Qed.
-
   (* TODO: Need this to be proven somewhere. *)
   Hypothesis auth_valid :
     forall a b, (✓ Auth (Excl a) b : iPropG Λ Σ) ⊑ (∃ b', a ≡ b ⋅ b').
-- 
GitLab