updating changelog

math-comp · Oct 1, 2024 · 0fef145 · 0fef145
1 parent 9dad92d
commit 0fef145
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -36,6 +36,15 @@
   + lemma `lt0_funenegM` renamed to `le0_funenegM`
     and hypothesis weakened from strict to large inequality
 
+- `theories/topology.v` split into `classical/filter.v` and `theories/topology.v`
+
+- moved from `topology.v` to `mathcomp_extra.v`:
+  + lemma `and_prop_in`
+
+- moved from `topology.v` to `set_interval.v`:
+  + lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP`
+  + lemmas `mem_inc_segment`, `mem_inc_segment`
+
 ### Renamed
 
 ### Generalized