Merge pull request #364 from math-comp/changelog.0.3.7

changelog for version 0.3.7

CHANGELOG.md

@@ -1,6 +1,107 @@
 # Changelog
 
-Last releases: [[0.3.6] - 2021-03-04](#036---2021-03-04) and [[0.3.5] - 2020-12-21](#035---2020-12-21)
+Last releases: [[0.3.7] - 2021-04-01](#037---2021-04-01) and [[0.3.6] - 2021-03-04](#036---2021-03-04)
+
+## [0.3.7] - 2021-04-01
+
+### 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`
+  + definition `dense` and lemma `denseNE`
+- 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`
+  + lemmas `has_sup1`, `has_inf1`
+- 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`
+  + 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`
+- 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 `nngnum.v`:
+  + instance `invr_nngnum`
+- in `posnum.v`:
+  + instance `posnum_nngnum`
+
+## Changed
+
+- in `ereal.v`:
+  + generalize lemma `lee_sum_nneg_subfset`
+  + lemmas `nbhs_oo_up_e1`, `nbhs_oo_down_e1`, `nbhs_oo_up_1e`, `nbhs_oo_down_1e`
+    `nbhs_fin_out_above`, `nbhs_fin_out_below`, `nbhs_fin_out_above_below`
+    `nbhs_fin_inbound`
+- in `sequences.v`:
+  + generalize lemmas `ereal_nondecreasing_series`, `is_cvg_ereal_nneg_series`,
+    `ereal_nneg_series_lim_ge0`, `ereal_nneg_series_pinfty`
+- in `measure.v`:
+  + generalize lemma `bigUB_of`
+  + generalize theorem `Boole_inequality`
+- in `classical_sets.v`:
+  + change the order of arguments of `subset_trans`
+
+- canonicals and coercions have been changed so that there is not need
+  anymore for explicit types casts to `R^o`, `[filteredType R^o of R^o]`,
+  `[filteredType R^o * R^o of R^o * R^o]`, `[lmodType R of R^o]`,
+  `[normedModType R of R^o]`,`[topologicalType of R^o]`, `[pseudoMetricType R of R^o]`
+- `sequences.v` now imports `numFieldNormedType.Exports`
+- `topology.v` now imports `reals`
+- `normedtype.v` now imports `vector`, `fieldext`, `falgebra`,
+  `numFieldTopology.Exports`
+- `derive.v` now imports `numFieldNormedType.Exports`
+
+### Renamed
+
+- in `ereal.v`:
+  + `is_realN` -> `fin_numN`
+  + `is_realD` -> `fin_numD`
+  + `ereal_sup_set0` -> `ereal_sup0`
+  + `ereal_sup_set1` -> `ereal_sup1`
+  + `ereal_inf_set0` -> `ereal_inf0`
+
+### Removed
+
+- in `topology.v`:
+  + section `numFieldType_canonical`
+- in `normedtype.v`:
+  + lemma `R_ball`
+  + definition `numFieldType_pseudoMetricNormedZmodMixin`
+  + canonical `numFieldType_pseudoMetricNormedZmodType`
+  + global instance `Proper_nbhs'_realType`
+  + lemma `R_normZ`
+  + definition `numFieldType_NormedModMixin`
+  + canonical `numFieldType_normedModType`
+- in `ereal.v`:
+  + definition `is_real`
 
 ## [0.3.6] - 2021-03-04
 

CHANGELOG_UNRELEASED.md

@@ -4,107 +4,12 @@
 
 ### 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`
-
 ### Changed
 
-- in `ereal.v`:
-  + generalize lemma `lee_sum_nneg_subfset`
-- in `sequences.v`:
-  + generalize lemmas `ereal_nondecreasing_series`, `is_cvg_ereal_nneg_series`,
-    `ereal_nneg_series_lim_ge0`, `ereal_nneg_series_pinfty`
-- in `measure.v`:
-  + generalize lemma `bigUB_of`
-  + generalize theorem `Boole_inequality`
-
-- canonicals and coercions have been changed so that there is not need
-  anymore for explicit types casts to `R^o`, `[filteredType R^o of R^o]`,
-  `[filteredType R^o * R^o of R^o * R^o]`, `[lmodType R of R^o]`,
-  `[normedModType R of R^o]`,`[topologicalType of R^o]`, `[pseudoMetricType R of R^o]`
-
-- `topology.v` now imports `reals`
-- `normedtype.v` now imports `vector`, `fieldext`, `falgebra`,
-  `numFieldTopology.Exports`
-- `derive.v` now imports `numFieldNormedType.Exports`
-- `sequences.v` now imports `numFieldNormedType.Exports`
-- in `ereal.v`:
-  + lemmas `nbhs_oo_up_e1`, `nbhs_oo_down_e1`, `nbhs_oo_up_1e`, `nbhs_oo_down_1e`
-    `nbhs_fin_out_above`, `nbhs_fin_out_below`, `nbhs_fin_out_above_below`
-    `nbhs_fin_inbound`
-- in `classical_sets.v`:
-  + change the order of arguments of `subset_trans`
-
 ### Renamed
 
-- in `ereal.v`:
-  + `is_realN` -> `fin_numN`
-  + `is_realD` -> `fin_numD`
-  + `ereal_sup_set0` -> `ereal_sup0`
-  + `ereal_sup_set1` -> `ereal_sup1`
-  + `ereal_inf_set0` -> `ereal_inf0`
-
 ### Removed
 
-- in `topology.v`:
-  + section `numFieldType_canonical`
-- in `normedtype.v`:
-  + lemma `R_ball`
-  + definition `numFieldType_pseudoMetricNormedZmodMixin`
-  + canonical `numFieldType_pseudoMetricNormedZmodType`
-  + global instance `Proper_nbhs'_realType`
-  + lemma `R_normZ`
-  + definition `numFieldType_NormedModMixin`
-  + canonical `numFieldType_normedModType`
-- in `ereal.v`:
-  + definition `is_real`
-
 ### Infrastructure
 
 ### Misc

INSTALL.md

@@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.3.6
+$ opam install coq-mathcomp-analysis.0.3.7
 ```
 4. Everytime you want to work in this same context, you need to type
 ```