diff --git a/CHANGELOG.md b/CHANGELOG.md
index dfd7190618e803197fcbbbc2f7f13f4417b96cbf..2a65cfe9e979d1ee78562e3c1dfd4b8e83a47b61 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -14,6 +14,7 @@ Coq 8.10 is no longer supported by this release.
 - Rename `Is_true_false` → `Is_true_false_2` and `eq_None_ne_Some` → `eq_None_ne_Some_1`.
 - Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext`.
 - Remove a spurious `Global Arguments Pos.of_nat : simpl never`.
+- Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.
 
 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 659f559b9ac07e9130943844a04fe65d25a35c63..65b56cfd5307f6bb2f59f4a1058ab44b805216d4 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -55,6 +55,17 @@ Proof. intros ?. rename select nat into m. exists m. done. Qed.
 Goal ∀ (P : nat → Prop), P 3 → P 4 → P 4.
 Proof. intros P **. rename select (P _) into HP4. apply HP4. Qed.
 
+Goal ∀ P Q : Prop, True ∨ True → P ∨ Q → Q ∨ P.
+Proof.
+  intros P Q ??. (* should select the last hypothesis *)
+  destruct select (_ ∨ _); by constructor.
+Restart.
+  intros P Q ??. (* should select the last hypothesis *)
+  destruct select (_ ∨ _) as [H1|H2].
+  - right. exact H1.
+  - left. exact H2.
+Qed.
+
 (** Regression tests for [naive_solver]. *)
 Lemma naive_solver_issue_115 (P : nat → Prop) (x : nat) :
   (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
diff --git a/theories/tactics.v b/theories/tactics.v
index 744ec4b71494275fee04328618bdeb0e32fc8442..2baea53c02596cc1c6053523658fa554a585345c 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -599,6 +599,11 @@ Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => rever
 Tactic Notation "rename" "select" open_constr(pat) "into" ident(name) :=
   select pat (fun H => rename H into name).
 
+Tactic Notation "destruct" "select" open_constr(pat) :=
+  select pat (fun H => destruct H).
+Tactic Notation "destruct" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
+  select pat (fun H => destruct H as ipat).
+
 (** The tactic [is_closed_term t] succeeds if [t] is a closed term and fails otherwise.
 By closed we mean that [t] does not depend on any variable bound in the context.
 axioms are considered closed terms by this tactic (but Section