diff --git a/CHANGELOG.md b/CHANGELOG.md
index e67fcf4d2976cc710b5dc9bfe0e3c80587ed10fc..beadd84c7496c9ab623105a76bcc431fed0caeb5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -24,6 +24,8 @@ Coq 8.11 is no longer supported.
 - Rename `map_disjoint_subseteq` → `kmap_subseteq` and
   `map_disjoint_subset` → `kmap_subset`.
 - Add `map_Exists` as an analogue to `map_Forall`. (by Michael Sammler)
+- Add `case_match eqn:H` that behaves like `case_match` but allows naming the
+  generated equality. (by Michael Sammler)
 
 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 65b56cfd5307f6bb2f59f4a1058ab44b805216d4..8272a6405107586878fe9f77c7fcaa9ef60b3d57 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -49,6 +49,22 @@ Proof.
   destruct_and?. Fail destruct_and!. assumption.
 Qed.
 
+(** Tests for [case_match] *)
+Goal ∀ n : nat, match n with | 0 => n = 0 | S n' => n = S n' end.
+Proof.
+  intros. by case_match.
+Restart.
+  intros. by case_match eqn:Heq; revert Heq. (* [revert Heq] checks that [Heq] exists *)
+Qed.
+
+Goal ∀ n m : nat, match n with | 0 => m = 0 | S n' => m = S n' end → n = m.
+Proof.
+  intros. by case_match.
+Restart.
+  intros. by case_match eqn:Heq; revert Heq. (* [revert Heq] checks that [Heq] exists *)
+Qed.
+
+(** Tests for [select] tactics *)
 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 79a5be4489f42b98d1c59b5e351031ca9a200c40..d4c143a6faf0c86a147470ceaac4025c744c7d4e 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -163,11 +163,14 @@ Tactic Notation "destruct_or" "!" :=
 (** The tactic [case_match] destructs an arbitrary match in the conclusion or
 assumptions, and generates a corresponding equality. This tactic is best used
 together with the [repeat] tactical. *)
-Ltac case_match :=
+Tactic Notation "case_match" "eqn" ":" ident(Hd) :=
   match goal with
-  | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:?
-  | |- context [ match ?x with _ => _ end ] => destruct x eqn:?
+  | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:Hd
+  | |- context [ match ?x with _ => _ end ] => destruct x eqn:Hd
   end.
+Ltac case_match :=
+  let H := fresh in case_match eqn:H.
+
 
 (** The tactic [unless T by tac_fail] succeeds if [T] is not provable by
 the tactic [tac_fail]. *)