From 34037c0fda5631cde8eadaeec8170ffd84020165 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 Jul 2016 16:31:19 +0200
Subject: [PATCH] Simplify TimelessElim class.

---
 proofmode/classes.v     | 2 +-
 proofmode/coq_tactics.v | 2 +-
 proofmode/pviewshifts.v | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/proofmode/classes.v b/proofmode/classes.v
index c25740c0c..50fdd54b6 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -314,5 +314,5 @@ Global Instance into_exist_always {A} P (Φ : A → uPred M) :
 Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
 
 Class TimelessElim (Q : uPred M) :=
-  timeless_elim `{!TimelessP P} R : (R ⊢ Q) → ▷ P ★ (P -★ R) ⊢ Q.
+  timeless_elim `{!TimelessP P} : ▷ P ★ (P -★ Q) ⊢ Q.
 End classes.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 3b3bb0f12..36f52d72a 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -382,7 +382,7 @@ Lemma tac_timeless Δ Δ' i p P Q :
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
-  rewrite always_if_later right_id. by apply timeless_elim.
+  by rewrite always_if_later right_id HQ timeless_elim.
 Qed.
 
 (** * Always *)
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 8695abb15..df3203323 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -32,8 +32,8 @@ Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
 
 Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q).
 Proof.
-  intros P ? R HR. rewrite (pvs_timeless E1 P) pvs_frame_r.
-  by rewrite wand_elim_r HR pvs_trans; last set_solver.
+  intros P ?. rewrite (pvs_timeless E1 P) pvs_frame_r.
+  by rewrite wand_elim_r pvs_trans; last set_solver.
 Qed.
 
 Class IsFSA {A} (P : iProp Λ Σ) (E : coPset)
@@ -57,7 +57,7 @@ Qed.
 Global Instance timeless_elim_fsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
   IsFSA Q E fsa fsaV Φ → TimelessElim Q.
 Proof.
-  intros ? P ? R. rewrite (is_fsa Q) -{2}fsa_pvs_fsa. intros <-.
+  intros ? P ?. rewrite (is_fsa Q) -{2}fsa_pvs_fsa.
   by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
 Qed.
 
-- 
GitLab