fix changelog

CHANGELOG_UNRELEASED.md

@@ -4,54 +4,6 @@
 
 ### Added
 
-- 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`,
-    `sumERFin`, `ereal_inf1`, `eqe_oppP`, `eqe_oppLRP`, `oppe_subset`,
-    `ereal_inf_pinfty`
-  + definition `er_map`
-  + definition `er_map`
-- in `classical_sets.v`:
-  + notation `[disjoint ... & ..]`
-  + lemmas `mkset_nil`, `bigcup_mkset`, `bigcup_nonempty`, `bigcup0`, `bigcup0P`,
-    `subset_bigcup_r`, `eqbigcup_r`, `eq_set_inl`, `set_in_in`
-- 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 `reals.v`:
-  + lemmas `has_sup1`, `has_inf1`
-- in `nngnum.v`:
-  + instance `invr_nngnum`
-- in `posnum.v`:
-  + instance `posnum_nngnum`
 - file `csum.v`:
   + lemma `ub_ereal_sup_adherent2`
   + definition `csum`, lemmas `csum0`, `csum_ge0`, `csum_fset`,

theories/csum.v

@@ -157,7 +157,7 @@ apply/eqP; rewrite eq_le; apply/andP; split.
     rewrite predeqE => i; split.
       move/fset0Pn => [t]; rewrite !inE /= => /andP[tF tJi].
       apply/imfsetP; exists t => //; rewrite /g.
-      (* utiliser les prop de triviset *) *)
+      (* use trivIset properties *) *)
   have : set_finite KFJ.
     suff suppFJ : set_finite [set k | FJ k != fset0].
       have KFJsuppF : KFJ `<=` [set k | FJ k != fset0] by move=> t [].