diff --git a/proofmode/classes.v b/proofmode/classes.v
index c25740c0c9c1663c832a2ac94b72beea773ae048..50fdd54b659a0806122fbc5ef6221b167a0e6fb1 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 3b3bb0f129fda78c3c36315d29df4e322e46078a..36f52d72a7ec20f72712fb6ad7cd31d7a0b472fe 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 8695abb15ce6943967504f3e8450b25da8c085c0..df3203323e96350820f988dab219d639f553fec6 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.