diff options
| author | Cyril Cohen | 2020-11-13 15:00:55 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-13 15:00:55 +0100 |
| commit | 1a098263b335ccc4cf72880662dccbe79185a8ab (patch) | |
| tree | 057f0c89a13a19aae6624bd1f235f9a3530b7f57 /CHANGELOG_UNRELEASED.md | |
| parent | 903f12374f8b388b8f28da6cad06724ae0bf5075 (diff) | |
| parent | 2f906481423530b03f21ff605aaee3f281131608 (diff) | |
Merge pull request #646 from pi8027/rename-eq_sorted
Rename `eq_sorted` lemmas to `sorted_eq` and generalize `sort_le_id`
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4b854c1..68eb6d5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -353,6 +353,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v`, generalized lemmas `sub_path_in`, `sub_sorted_in`, and `eq_path_in` for non-`eqType`s. +- in `order.v`, generalized `sort_le_id` for any `porderType`. + ### Renamed - `big_rmcond` -> `big_rmcond_in` (cf Changed section) @@ -400,6 +402,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). (`allpairs_consr` and `allpairs_catr` are now deprecated alias, and will be attributed to the new `perm_allpairs_catr`). +- in `path.v`, `eq_sorted(_irr)` -> `(irr_)sorted_eq` + - in `div.v` + `coprime_mul(l|r)` -> `coprimeM(l|r)` + `coprime_exp(l|r)` -> `coprimeX(l|r)` @@ -414,6 +418,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + `primes_(mul|exp)` -> `primes(M|X)` + `pnat_(mul|exp)` -> `pnat(M|X)` +- in `order.v`, `eq_sorted_(le|lt)` -> `(le|lt)_sorted_eq` + - in `ssralg.v` + `prodrMn` has been renamed `prodrMn_const` (with deprecation alias, cf. Added section) |