aboutsummaryrefslogtreecommitdiff
path: root/CHANGELOG_UNRELEASED.md
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
-rw-r--r--CHANGELOG_UNRELEASED.md2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ad3cae2..1e779c3 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -22,6 +22,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
- in `path.v`, new lemmas: `sorted_pairwise(_in)`, `path_pairwise(_in)`,
`cycle_all2rel(_in)`, `pairwise_sort`, and `sort_pairwise_stable`.
+- in `interval.v`, new lemmas: `ge_pinftyE`, `le_ninftyE`, `gt_pinfty`, `lt_ninfty`.
+
### Changed
- In `ssralg.v` and `ssrint.v`, the nullary ring notations `-%R`, `+%R`, `*%R`,