From 924782c8bd018b0073467fd292baaeb85ec0f5f9 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 16 Dec 2021 13:53:22 +0100 Subject: [PATCH] CHANGELOG. --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index dfd71906..2a65cfe9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,6 +14,7 @@ Coq 8.10 is no longer supported by this release. - Rename `Is_true_false` → `Is_true_false_2` and `eq_None_ne_Some` → `eq_None_ne_Some_1`. - Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext`. - Remove a spurious `Global Arguments Pos.of_nat : simpl never`. +- Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`. The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). -- GitLab