aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorReynald Affeldt2020-06-04 22:55:59 +0900
committerCyril Cohen2020-06-06 19:39:35 +0200
commit19a798cfaaa7875e7406c0283166fb5a97a0153c (patch)
tree386e1aa102349bcc77ff67e5236089182fd2d165
parent0a4c927087ef2c3f6f0e20f6ad65ca932d9d3f6d (diff)
fix the changelog
-rw-r--r--CHANGELOG_UNRELEASED.md7
1 files changed, 4 insertions, 3 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 6f26e81..edf32ff 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -65,9 +65,6 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
- in `ssrbool.v`
+ lemmas about the `cancel` predicate and `{in _, _}`/`{on _, _}` notations:
* `onW_can`, `onW_can_in`, `in_onW_can`, `onT_can`, `onT_can_in`, `in_onT_can`
- + lemmas about monotone functions and the `{in _, _}` notation:
- * `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`, `monoRL_in`,
- `can_mono_in`
+ lemmas about the `cancel` predicate and injective functions:
* `inj_can_sym_in_on`, `inj_can_sym_on`, `inj_can_sym_in`
@@ -107,6 +104,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
+ `ltxU` -> `lt_maxr`
+ `lexU` -> `le_maxr`
+- in `ssrbool.v`
+ + lemmas about monotone functions and the `{in _, _}` notation:
+ * `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`, `monoRL_in`, `can_mono_in`
+
### Renamed
- in `fintype` we deprecate and rename the following: