changelog

math-comp · Jul 29, 2024 · 9a942f1 · 9a942f1
1 parent 191da25
commit 9a942f1
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -43,6 +43,9 @@
   + lemmas `lteD2rE`, `leeD2rE`
   + lemmas `lte_dD2rE`, `lee_dD2rE`
 
+- in `classical_sets.v`:
+  + lemmas `xsectionP`, `ysectionP`
+
 ### Changed
 
 - in `topology.v`:
@@ -146,6 +149,9 @@
   + lemmas `floor0`, `floor1`
   + lemma `le_floor` (use `Num.Theory.floor_le` instead)
 
+- in `topology.v`, `function_spaces.v`, `normedtype.v`:
+  + local notation `to_set`
+
 ### Infrastructure
 
 ### Misc