aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorChristian Doczkal2020-09-10 18:54:07 +0200
committerChristian Doczkal2020-09-29 11:10:31 +0200
commit544d89a7711be2f25c3a845130e5cede590bc766 (patch)
treecd41f476ad660c1976a224d1e2bceedf7bf91bb9
parent94e1bf37bbdabe3f2cf300e60a8c4eb856aa4819 (diff)
CHANGELOG entries
-rw-r--r--CHANGELOG_UNRELEASED.md5
1 files changed, 4 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 130b98e..faeafd0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -40,7 +40,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
- in `finset.v`, new lemmas: `properC`, `properCr`, `properCl`
- in `ssrnat.v`, new lemmas: `subn_minl`, `subn_maxl`
- in `ssrnat.v`, new lemma: `oddS`
-
+- in `finset.v`, new lemmas: `mem_imset_eq`, `mem_imset2_eq`.
+ These lemmas will lose the `_eq` suffix in the next release, when the shortende names will become availabe (cf. Renamed section)
- Added a factory `distrLatticePOrderMixin` in order.v to build a
`distrLatticeType` from a `porderType`.
@@ -237,6 +238,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
### Renamed
- `big_rmcond` -> `big_rmcond_in` (cf Changed section)
+- `mem_imset` -> `imset_f` (with deprecation alias, cf. Added section)
+- `mem_imset2` -> imset2_f` (with deprecation alias, cf. Added section)
- in `interval.v`, we deprecate, rename, and relocate to `order.v` the following:
+ `lersif_(trans|anti)` -> `lteif_(trans|anti)`