changelog for version 0.3.0

math-comp · May 26, 2020 · f3ec99e · f3ec99e
1 parent 244f131
commit f3ec99e
Show file tree

Hide file tree

Showing 2 changed files with 74 additions and 72 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,17 +1,89 @@
 # Changelog
 
-## [0.3.0] - 2020-05-??
+Last release: [[0.3.0] - 2020-05-26](#030---2020-05-26)
 
-This release is compatible with MathComp version 1.11.0+beta1
+## [0.3.0] - 2020-05-26
+
+This release is compatible with MathComp version 1.11.0+beta1.
+
+The biggest change of this release is compatibility with MathComp
+1.11.0.  The latter introduces in particular ordered types. The
+notation for the norm is now uniform.
 
 ### Added
 
+- `sequences.v`: Main theorems about sequences and series, and examples
+  + Definitions:
+    * `[sequence E]_n` is a special notation for `fun n => E`
+    * `series u_` is the sequence of partial sums
+    * `[normed S]` is the series of absolute values, if S is a series
+    * `harmonic` is the name of a sequence,
+       apply `series` to them to get the series.
+  + Theorems:
+    * lots of helper lemmas to prove convergence of sequences
+    * convergence of harmonic sequence
+    * convergence of a series implies convergence of a sequence
+    * absolute convergence implies convergence of series
+- in `ereal.v`: lemmas about extended reals' arithmetic
+- in `normedtype.v`: Definitions and lemmas about generic domination,
+  boundedness, and lipschitz
+  + See header for the notations and their localization
+  + Added a bunch of combinators to extract existential witnesses
+  + Added `filter_forall` (commutation between a filter and finite forall)
+- about extended reals:
+  + equip extended reals with a structure of topological space
+  + show that extended reals are hausdorff
+- in `topology.v`, predicate `close`
+- lemmas about bigmaxr and argmaxr
+  + `\big[max/x]_P F = F [arg max_P F]`
+  + similar lemma for `bigmin`
+- lemmas for `within`
+- add `setICl` (intersection of set with its complement)
+- `prodnormedzmodule.v`
+  + `ProdNormedZmodule` transfered from MathComp
+  + `nonneg` type for non-negative numbers
+- `bigmaxr`/`bigminr` library
+- Lemmas `interiorI`, `setCU` (complement of union is intersection of complements),
+  `setICl`, `nonsubset`, `setC0`, `setCK`, `setCT`, `preimage_setI/U`, lemmas about `image`
+
 ### Changed
 
+- in `Rstruct.v`, `bigmaxr` is now defined using `bigop`
+- `inE` now supports `in_setE` and `in_fsetE`
+- fix the definition of `le_ereal`, `lt_ereal`
+- various generalizations to better use the hierarchy of `ssrnum` (`numDomainType`,
+  `numFieldType`, `realDomainType`, etc. when possible) in `topology.v`,
+  `normedtype.v`, `derive.v`, etc.
+
 ### Renamed
 
+- renaming `flim` to `cvg`
+  + `cvg` corresponds to `_ --> _`
+  + `lim` corresponds to `lim _`
+  + `continuous`  corresponds to continuity
+  + some suffixes `_opp`, `_add` ... renamed to `N`, `D`, ...
+- big refactoring about naming conventions
+  + complete the theory of `cvg_`, `is_cvg_` and `lim_` in normedtype.v
+    with consistent naming schemes
+  + fixed differential of `inv` which was defined on `1 / x` instead of `x^-1`
+  + two versions of lemmas on inverse exist
+    * one in realType (`Rinv_` lemmas), for which we have differential
+    * a general one `numFieldType`  (`inv_` lemmas in normedtype.v, no differential so far, just continuity)
+  + renamed `cvg_norm` to `cvg_dist` to reuse the name `cvg_norm` for
+    convergence under the norm
+- `Uniform` renamed to `PseudoMetric`
+- rename `is_prop` to `is_subset1`
+
 ### Removed
 
+- `sub_trans` (replaced by MathComp's `subrKA`)
+- `derive.v` does not require `Reals` anymore
+- `Rbar.v` is almost not used anymore
+
 ### Infrastructure
 
+- NIX support
+  + see `config.nix`, `default.nix`
+  + for the CI also
+
 ### Misc
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -2,84 +2,14 @@
 
 ## [Unreleased]
 
-The biggest change of this release is compatibility with MathComp
-1.11.0.  The latter introduces in particular ordered types. The
-notation for the norm is now uniform.
-
 ### Added
 
-- `sequences.v`: Main theorems about sequences and series, and examples
-  + Definitions:
-    * `[sequence E]_n` is a special notation for `fun n => E`
-    * `series u_` is the sequence of partial sums
-    * `[normed S]` is the series of absolute values, if S is a series
-    * `harmonic` is the name of a sequence,
-       apply `series` to them to get the series.
-  + Theorems:
-    * lots of helper lemmas to prove convergence of sequences
-    * convergence of harmonic sequence
-    * convergence of a series implies convergence of a sequence
-    * absolute convergence implies convergence of series
-- in `ereal.v`: lemmas about extended reals' arithmetic
-- in `normedtype.v`: Definitions and lemmas about generic domination,
-  boundedness, and lipschitz
-  + See header for the notations and their localization
-  + Added a bunch of combinators to extract existential witnesses
-  + Added `filter_forall` (commutation between a filter and finite forall)
-- about extended reals:
-  + equip extended reals with a structure of topological space
-  + show that extended reals are hausdorff
-- in `topology.v`, predicate `close`
-- lemmas about bigmaxr and argmaxr
-  + `\big[max/x]_P F = F [arg max_P F]`
-  + similar lemma for `bigmin`
-- lemmas for `within`
-- add `setICl` (intersection of set with its complement)
-- `prodnormedzmodule.v`
-  + `ProdNormedZmodule` transfered from MathComp
-  + `nonneg` type for non-negative numbers
-- `bigmaxr`/`bigminr` library
-- Lemmas `interiorI`, `setCU` (complement of union is intersection of complements),
-  `setICl`, `nonsubset`, `setC0`, `setCK`, `setCT`, `preimage_setI/U`, lemmas about `image`
-
 ### Changed
 
-- in `Rstruct.v`, `bigmaxr` is now defined using `bigop`
-- `inE` now supports `in_setE` and `in_fsetE`
-- fix the definition of `le_ereal`, `lt_ereal`
-- various generalizations to better use the hierarchy of `ssrnum` (`numDomainType`,
-  `numFieldType`, `realDomainType`, etc. when possible) in `topology.v`,
-  `normedtype.v`, `derive.v`, etc.
-
 ### Renamed
 
-- renaming `flim` to `cvg`
-  + `cvg` corresponds to `_ --> _`
-  + `lim` corresponds to `lim _`
-  + `continuous`  corresponds to continuity
-  + some suffixes `_opp`, `_add` ... renamed to `N`, `D`, ...
-- big refactoring about naming conventions
-  + complete the theory of `cvg_`, `is_cvg_` and `lim_` in normedtype.v
-    with consistent naming schemes
-  + fixed differential of `inv` which was defined on `1 / x` instead of `x^-1`
-  + two versions of lemmas on inverse exist
-    * one in realType (`Rinv_` lemmas), for which we have differential
-    * a general one `numFieldType`  (`inv_` lemmas in normedtype.v, no differential so far, just continuity)
-  + renamed `cvg_norm` to `cvg_dist` to reuse the name `cvg_norm` for
-    convergence under the norm
-- `Uniform` renamed to `PseudoMetric`
-- rename `is_prop` to `is_subset1`
-
 ### Removed
 
-- `sub_trans` (replaced by MathComp's `subrKA`)
-- `derive.v` does not require `Reals` anymore
-- `Rbar.v` is almost not used anymore
-
 ### Infrastructure
 
-- NIX support
-  + see `config.nix`, `default.nix`
-  + for the CI also
-
 ### Misc