From 00e29c8b3e31f99fde74c9cdb7fbaf791fd9ebcd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 Jan 2021 12:43:17 +0100
Subject: [PATCH] remove unused find_pat tactic

---
 CHANGELOG.md       |  1 +
 theories/tactics.v | 11 -----------
 2 files changed, 1 insertion(+), 11 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index cb181a52..63f94233 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 c1ac9116..cc9db99b 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
-- 
GitLab