preparing changelog (#227)

CHANGELOG.md

@@ -1,13 +1,38 @@
 # Changelog
 
-Last release: [[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
+
+### 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

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