Skip to content
Snippets Groups Projects
Commit 924782c8 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

CHANGELOG.

parent 723ad25f
No related branches found
No related tags found
1 merge request!352Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.
Pipeline #58955 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 0 deletions
CHANGELOG.md
+ 1
− 0
View file @ 924782c8
......@@ -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`).
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment