diff --git a/CHANGELOG.md b/CHANGELOG.md
index f18adbf9af8b4c295dffac47961824d4440683fe..cec2faf06f2d4d42956a1daaf877effd80e86510 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -30,6 +30,8 @@ Coq 8.19 is newly supported by this version of std++.
 - Add lemma `join_app`.
 - Allow patterns and type annotations in `propset` notation, e.g.,
   `{[ (x, y) : nat * nat | x = y ]}`. (by Thibaut Pérami)
+- Add `inv select` and `inversion select` tactics that allow selecting the
+  to-be-inverted hypothesis with a pattern.
 
 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/stdpp/tactics.v b/stdpp/tactics.v
index 0d29cfe1d94c544f714b3d0a9a3b21346ea4f16f..f3639f00c03794d262d6016343f6fbfb1ef628dc 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -774,6 +774,9 @@ Tactic Notation "select" open_constr(pat) tactic3(tac) :=
       so then shelved goals are produced for every such evar. *)
   | H : pat |- _ => let T := (type of H) in unify T pat; tac H
   end.
+
+(** We provide [select] variants of some widely used tactics. *)
+
 (** [select_revert] reverts the first hypothesis matching [pat]. *)
 Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => revert H).
 
@@ -785,6 +788,15 @@ Tactic Notation "destruct" "select" open_constr(pat) :=
 Tactic Notation "destruct" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
   select pat (fun H => destruct H as ipat).
 
+Tactic Notation "inversion" "select" open_constr(pat) :=
+  select pat (fun H => inversion H).
+Tactic Notation "inversion" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
+  select pat (fun H => inversion H as ipat).
+Tactic Notation "inv" "select" open_constr(pat) :=
+  select pat (fun H => inv H).
+Tactic Notation "inv" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
+  select pat (fun H => inv 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
diff --git a/tests/tactics.v b/tests/tactics.v
index bd7050ea4f21981359e968ac267250dd904e555b..847bf3b994c7aaab0b1c47327ef1530dd20ec1ce 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -79,13 +79,35 @@ 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 *)
+  intros P Q ??.
+  (* should select the last hypothesis *)
   destruct select (_ ∨ _); by constructor.
 Restart.
-  intros P Q ??. (* should select the last hypothesis *)
+  intros P Q ??.
+  (* should select the last hypothesis *)
   destruct select (_ ∨ _) as [H1|H2].
   - right. exact H1.
   - left. exact H2.
+Restart.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inv select (_ ∨ _); by constructor.
+Restart.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inv select (_ ∨ _) as [H1|H2].
+  - right. exact H1.
+  - left. exact H2.
+Restart.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inversion select (_ ∨ _); by constructor.
+Restart.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inversion select (_ ∨ _) as [H1|H2].
+  - right. exact H1.
+  - left. exact H2.
 Qed.
 
 (** [mk_evar] works on things that coerce to types. *)