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

CHANGELOG.

parent 6c4dede0
No related branches found
No related tags found
1 merge request!453Improve `bijective_finite`.
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
CHANGELOG.md
+ 2
− 0
View file @ b8b45764
...@@ -19,6 +19,8 @@ Coq 8.12 and 8.13 are no longer supported by this release. ...@@ -19,6 +19,8 @@ Coq 8.12 and 8.13 are no longer supported by this release.
- Add lemmas `Nat.mul_reg_{l,r}` for cancellation of multiplication on `nat`. - Add lemmas `Nat.mul_reg_{l,r}` for cancellation of multiplication on `nat`.
(Names are analogous to the `Z.` lemmas for Coq's standard library.) (Names are analogous to the `Z.` lemmas for Coq's standard library.)
- Rename `map_preimage` into `map_preimg` to be consistent with `dom`. - Rename `map_preimage` into `map_preimg` to be consistent with `dom`.
- Improve `bijective_finite`: do not require an inverse, no not unnecessarily
remove duplicates.
The following `sed` script should perform most of the renaming The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). (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.
Please register or to comment