changelog

math-comp · Aug 1, 2024 · 3de3c6e · 3de3c6e
1 parent 02c2962
commit 3de3c6e
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -110,6 +110,8 @@
     `parameterized_integral_left`, `parameterized_integral_cvg_at_left`,
     `parameterized_integral_continuous`
   + corollary `continuous_FTC2`
+- in `classical_sets.v`:
+  + lemmas `xsectionP`, `ysectionP`
 
 ### Changed
 
@@ -238,6 +240,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