diff --git a/CHANGELOG.md b/CHANGELOG.md
index cb181a5209c0785a68e2ac0d13a4ed1055cb40fa..63f9423395ed94888359237d1d5f4e59be16f86d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -45,6 +45,7 @@ Coq 8.8 and 8.9 are no longer supported.
 - 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.
+- Remove unused `find_pat` tactic that was made mostly obsolete by `select`.
 
 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/theories/tactics.v b/theories/tactics.v
index c1ac9116df7cd08cc5fc0ad173e4ddac67ceb3d6..cc9db99bc306da1323cea35b1023174c76444e03 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -508,17 +508,6 @@ Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
 Ltac unblock_goal := unfold block in *.
 
 
-(** The following tactic can be used to add support for patterns to tactic notation:
-It will search for the first subterm of the goal matching [pat], and then call [tac]
-with that subterm. *)
-Ltac find_pat pat tac :=
-  match goal with
-  |- context [?x] =>
-      unify pat x with typeclass_instances;
-      tryif tac x then idtac else fail 2
-  end.
-
-
 (** [select] finds the first hypothesis matching [pat] and passes it
 to the continuation [tac]. Its main advantage over using [match goal
 with ] directly is that it is shorter. If [pat] matches multiple