From bfa3f98db1e9f319fc3d047372e1ccc065c2e628 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 22 Apr 2021 21:01:00 +0900
Subject: [PATCH] fix changelog

---
 CHANGELOG_UNRELEASED.md | 38 --------------------------------------
 1 file changed, 38 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c3cdcb790e..f46fd6ebae 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -8,44 +8,6 @@
   + lemmas `big_nat_widenl`, `big_geq_mkord`
   + lemmas `lee_sum_nneg_natr`, `lee_sum_nneg_natl`
   + lemmas `fun_big_mkord`, `lee_sum_nneg_natr`, `lee_sum_nneg_natl`
-- in `topology.v`:
-  + global instance `ball_filter`
-  + module `regular_topology` with an `Exports` submodule
-    * canonicals `pointedType`, `filteredType`, `topologicalType`,
-      `uniformType`, `pseudoMetricType`
-  + module `numFieldTopology` with an `Exports` submodule
-    * many canonicals and coercions
-  + global instance `Proper_nbhs'_regular_numFieldType`
-- in `normedtype.v`:
-  + definitions `ball_`, `pointed_of_zmodule`, `filtered_of_normedZmod`
-  + lemmas `ball_norm_center`, `ball_norm_symmetric`, `ball_norm_triangle`
-  + definition `pseudoMetric_of_normedDomain`
-  + lemma `nbhs_ball_normE`
-  + global instances `Proper_nbhs'_numFieldType`, `Proper_nbhs'_realType`
-  + module `regular_topology` with an `Exports` submodule
-    * canonicals `pseudoMetricNormedZmodType`, `normedModType`.
-  + module `numFieldNormedType` with an `Exports` submodule
-    * many canonicals and coercions
-    * exports `Export numFieldTopology.Exports`
-  + canonical `R_regular_completeType`, `R_regular_CompleteNormedModule`
-- in `reals.v`:
-  + lemmas `Rfloor_lt0`, `floor_lt0`, `ler_floor`, `ceil_gt0`, `ler_ceil`
-- in `ereal.v`:
-  + lemmas `ereal_ballN`, `le_ereal_ball`, `ereal_ball_ninfty_oversize`,
-    `contract_ereal_ball_pinfty`, `expand_ereal_ball_pinfty`,
-    `contract_ereal_ball_fin_le`, `contract_ereal_ball_fin_lt`,
-    `expand_ereal_ball_fin_lt`, `ball_ereal_ball_fin_lt`, `ball_ereal_ball_fin_le`
-- in `classical_sets.v`:
-  + notation `[disjoint ... & ..]`
-  + lemmas `mkset_nil`, `bigcup_mkset`, `bigcup_nonempty`, `bigcup0`, `bigcup0P`,
-    `subset_bigcup_r`, `eqbigcup_r`
-- in `ereal.v`:
-  + lemmas `adde_undefC`, `real_of_erD`, `fin_num_add_undef`, `addeK`,
-    `subeK`, `subee`, `sube_le0`, `lee_sub`
-  + lemmas `addeACA`, `muleC`, `mule1`, `mul1e`, `abseN`
-  + enable notation `x \is a fin_num`
-    * definition `fin_num`, fact `fin_num_key`, lemmas `fin_numE`, `fin_numP`
-  + definition `dense` and lemma `denseNE`
 - in `measure.v`:
   + lemma `eq_bigcupB_of_bigsetU`
   + definition `caratheodory_measurable`, notation `... .-measurable`