diff --git a/CHANGELOG.md b/CHANGELOG.md
index e8d13a8eb18600b4f1bf9f8dc53d2c9589b05ce2..cb181a5209c0785a68e2ac0d13a4ed1055cb40fa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -43,6 +43,8 @@ Coq 8.8 and 8.9 are no longer supported.
 - Rename `seq_S_end_app` to `seq_S`. (The lemma `seq_S` is also in Coq's stdlib
   since Coq 8.12.)
 - Remove `omega` import and hint database in `tactics` file.
+- Add `rename select <pat> into <name>` tactic to find a hypothesis by pattern
+  and give it a fixed name.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/tests/tactics.v b/tests/tactics.v
index a606dbce49240e9ab1c77b09021650da74a93531..c2170c89a735642f69540f7046de55722c1cfaa8 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -1,6 +1,6 @@
 From stdpp Require Import tactics.
 
-Goal forall P1 P2 P3 P4 (P: Prop),
+Goal ∀ P1 P2 P3 P4 (P: Prop),
   P1 ∨ (Is_true (P2 || P3)) ∨ P4 →
   (P1 → P) →
   (P2 → P) →
@@ -12,7 +12,7 @@ Proof.
   destruct_or? HH; [ exact (X1 HH) | exact (X2 HH) | exact (X3 HH) | exact (X4 HH) ].
 Qed.
 
-Goal forall P1 P2 P3 P4 (P: Prop),
+Goal ∀ P1 P2 P3 P4 (P: Prop),
   P1 ∨ P2 →
   P3 ∨ P4 →
   (P1 → P3 → P) →
@@ -25,7 +25,7 @@ Proof.
   destruct_or?; [ exact (X1 HH1 HH2) | exact (X3 HH1 HH2) | exact (X2 HH1 HH2) | exact (X4 HH1 HH2) ].
 Qed.
 
-Goal forall P1 P2 P3 P4 (P: Prop),
+Goal ∀ P1 P2 P3 P4 (P: Prop),
   id (P1 ∨ P2) →
   id (P3 ∨ P4) →
   (P1 → P3 → P) →
@@ -41,10 +41,13 @@ Proof.
   [ exact (X1 HH1 HH2) | exact (X2 HH1 HH2) | exact (X3 HH1 HH2) | exact (X4 HH1 HH2) ].
 Qed.
 
-Goal forall P1 P2 P3 P4,
+Goal ∀ P1 P2 P3 P4,
   P1 ∧ (Is_true (P2 && P3)) ∧ P4 →
   P1 ∧ P2 ∧ P3.
 Proof.
   intros * HH. split_and!; [ destruct_and? HH; assumption | destruct_and?; assumption | ].
   destruct_and?. Fail destruct_and!. assumption.
 Qed.
+
+Goal ∀ (n : nat), ∃ m : nat, True.
+Proof. intros ?. rename select nat into m. exists m. done. Qed.
diff --git a/theories/tactics.v b/theories/tactics.v
index b635bdf73d802d22976177691d39f19f52ff5248..c1ac9116df7cd08cc5fc0ad173e4ddac67ceb3d6 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -537,6 +537,9 @@ Tactic Notation "select" open_constr(pat) tactic3(tac) :=
 (** [select_revert] reverts the first hypothesis matching [pat]. *)
 Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => revert H).
 
+Tactic Notation "rename" "select" open_constr(pat) "into" ident(name) :=
+  select pat (fun H => rename H into name).
+
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In
 particular, on those generated by the tactic [unfold_elem_ofs] which is used
 to solve propositions on sets. The [naive_solver] tactic implements an