From 97dc43937b29fb67f4f422662d4e25f71051c87a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 15 Jun 2016 16:50:45 +0200
Subject: [PATCH] Use projections in the instance of Timeless for pairs

---
 algebra/cofe.v        | 6 +++---
 program_logic/boxes.v | 5 -----
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index a624a12fc..96ac25d19 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -323,9 +323,9 @@ Section product.
       apply (conv_compl n (chain_map snd c)).
   Qed.
   Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin.
-  Global Instance pair_timeless (x : A) (y : B) :
-    Timeless x → Timeless y → Timeless (x,y).
-  Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
+  Global Instance prod_timeless (x : A * B) :
+    Timeless (x.1) → Timeless (x.2) → Timeless x.
+  Proof. by intros ???[??]; split; apply (timeless _). Qed.
   Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC.
   Proof. intros ?? [??]; apply _. Qed.
 End product.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 9f5053960..84bc45374 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -57,11 +57,6 @@ Proof. solve_proper. Qed.
 Global Instance slice_persistent γ P : PersistentP (slice N γ P).
 Proof. apply _. Qed.
 
-(* This should go automatic *)
-Instance box_own_auth_timeless γ
-  (a : auth (option (excl bool))) : TimelessP (box_own_auth γ a).
-Proof. apply own_timeless, pair_timeless; apply _. Qed.
-
 Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) ⊢ b1 = b2.
 Proof.
-- 
GitLab