From a37d39429df38c0310b9a1734e043d7f9dd6b92e Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Jun 2020 05:08:53 +0200 Subject: [PATCH 1/2] preparing changelog --- CHANGELOG.md | 31 ++++++++++++++++++++++++++++--- CHANGELOG_UNRELEASED.md | 19 ------------------- 2 files changed, 28 insertions(+), 22 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e6a422c9cb..b880c55eaa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,13 +1,38 @@ # Changelog -Last release: [[0.3.0] - 2020-05-26](#030---2020-05-26) +Last release: [[0.3.1] - 2020-06-11](#031---2020-06-11) and [[0.3.0] - 2020-05-26](#030---2020-05-26) + +## [0.3.1] - 2020-06-11 + +### Added + +- in `boolp.v`, lemmas for classical reasoning `existsNP`, `existsPN`, + `forallNP`, `forallPN`, `Nimply`, `orC`. +- in `classical_sets.v`, definitions for supremums: `ul`, `lb`, + `supremum` +- in `ereal.v`: + + technical lemmas `lee_ninfty_eq`, `lee_pinfty_eq`, `lte_subl_addr`, `eqe_oppLR` + + lemmas about supremum: `ereal_supremums_neq0` + + definitions: + * `ereal_sup`, `ereal_inf` + + lemmas about `ereal_sup`: + * `ereal_sup_ub`, `ub_ereal_sup`, `ub_ereal_sup_adherent` +- in `normedtype.v`: + + function `contract` (bijection from `{ereal R}` to `R`) + + function `expand` (that cancels `contract`) + + `ereal_pseudoMetricType R` + +### Changed + +- in `reals.v`, `pred` replaced by `set` from `classical_sets.v` + + change propagated in many files ## [0.3.0] - 2020-05-26 -This release is compatible with MathComp version 1.11.0+beta1. +This release is compatible with MathComp version 1.11+beta1. The biggest change of this release is compatibility with MathComp -1.11.0. The latter introduces in particular ordered types. +1.11+beta1. The latter introduces in particular ordered types. All norms and absolute values have been unified, both in their denotation `|_| and in their theory. ### Added diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2e0084a7ac..c1ee5bdc82 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,27 +4,8 @@ ### Added -- in `boolp.v`, lemmas for classical reasoning `existsNP`, `existsPN`, - `forallNP`, `forallPN`, `Nimply`, `orC`. -- in `classical_sets.v`, definitions for supremums: `ul`, `lb`, - `supremum` -- in `ereal.v`: - + technical lemmas `lee_ninfty_eq`, `lee_pinfty_eq`, `lte_subl_addr`, `eqe_oppLR` - + lemmas about supremum: `ereal_supremums_neq0` - + definitions: - * `ereal_sup`, `ereal_inf` - + lemmas about `ereal_sup`: - * `ereal_sup_ub`, `ub_ereal_sup`, `ub_ereal_sup_adherent` -- in `normedtype.v`: - + function `contract` (bijection from `{ereal R}` to `R`) - + function `expand` (that cancels `contract`) - + `ereal_pseudoMetricType R` - ### Changed -- in `reals.v`, `pred` replaced by `set` from `classical_sets.v` - + change propagated in many files - ### Renamed ### Removed From d9923c23d75fbe55e63fb16762139c1addbf7b29 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Jun 2020 05:10:18 +0200 Subject: [PATCH 2/2] fixup --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b880c55eaa..ec059944aa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,6 @@ # Changelog -Last release: [[0.3.1] - 2020-06-11](#031---2020-06-11) and [[0.3.0] - 2020-05-26](#030---2020-05-26) +Last releases: [[0.3.1] - 2020-06-11](#031---2020-06-11) and [[0.3.0] - 2020-05-26](#030---2020-05-26) ## [0.3.1] - 2020-06-11