Skip to content
Snippets Groups Projects

remove unused find_pat tactic

Merged remove unused find_pat tactic
ralf/find_pat into master
Merged Ralf Jung requested to merge ralf/find_pat into master
Compare
and
2 files
+ 1
− 11
Compare changes
  • Side-by-side
  • Inline
Files
2
CHANGELOG.md
+ 1
− 0
@@ -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`):