diff --git a/CHANGELOG.md b/CHANGELOG.md
index 396f0b67b..2d18c75c7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,67 @@
 # Changelog
 
-Last releases: [[0.4.0] - 2022-03-08](#040---2022-03-08) and [[0.3.13] - 2022-01-24](#0313---2022-01-24)
+Last releases: [[0.5.0] - 2022-03-23](#050---2022-03-23) and [[0.4.0] - 2022-03-08](#040---2022-03-08)
+
+## [0.5.0] - 2022-03-23
+
+### Added
+
+- in `signed.v`:
+  + notations `%:nngnum` and `%:posnum`
+- in `ereal.v`:
+  + notations `{posnum \bar R}` and `{nonneg \bar R}`
+  + notations `%:pos` and `%:nng` in `ereal_dual_scope` and `ereal_scope`
+  + variants `posnume_spec` and `nonnege_spec`
+  + definitions `posnume`, `nonnege`, `abse_reality_subdef`,
+    `ereal_sup_reality_subdef`, `ereal_inf_reality_subdef`
+  + lemmas `ereal_comparable`, `pinfty_snum_subproof`, `ninfty_snum_subproof`,
+    `EFin_snum_subproof`, `fine_snum_subproof`, `oppe_snum_subproof`,
+    `adde_snum_subproof`, `dadde_snum_subproof`, `mule_snum_subproof`,
+    `abse_reality_subdef`, `abse_snum_subproof`, `ereal_sup_snum_subproof`,
+    `ereal_inf_snum_subproof`, `num_abse_eq0`, `num_lee_maxr`, `num_lee_maxl`,
+    `num_lee_minr`, `num_lee_minl`, `num_lte_maxr`, `num_lte_maxl`,
+    `num_lte_minr`, `num_lte_minl`, `num_abs_le`, `num_abs_lt`,
+    `posnumeP`, `nonnegeP`
+  + signed instances `pinfty_snum`, `ninfty_snum`, `EFin_snum`, `fine_snum`,
+    `oppe_snum`, `adde_snum`, `dadde_snum`, `mule_snum`, `abse_snum`,
+    `ereal_sup_snum`, `ereal_inf_snum`
+
+### Changed
+
+- in `functions.v`:
+  + `addrfunE` renamed to `addrfctE` and generalized to `Type`, `zmodType`
+  + `opprfunE` renamed to `opprfctE` and generalized to `Type`, `zmodType`
+- moved from `functions.v` to `classical_sets.v`
+  + lemma `subsetW`, definition `subsetCW`
+- in `mathcomp_extra.v`:
+  + fix notation `ltLHS`
+
+### Renamed
+
+- in `topology.v`:
+  + `open_bigU` -> `bigcup_open`
+- in `functions.v`:
+  + `mulrfunE` -> `mulrfctE`
+  + `scalrfunE` -> `scalrfctE`
+  + `exprfunE` -> `exprfctE`
+  + `valLr` -> `valR`
+  + `valLr_fun` -> `valR_fun`
+  + `valLrK` -> `valRK`
+  + `oinv_valLr` -> `oinv_valR`
+  + `valLr_inj_subproof` -> `valR_inj_subproof`
+  + `valLr_surj_subproof` -> `valR_surj_subproof`
+- in `measure.v`:
+  + `measurable_bigcup` -> `bigcupT_measurable`
+  + `measurable_bigcap` -> `bigcapT_measurable`
+  + `measurable_bigcup_rat` -> `bigcupT_measurable_rat`
+- in `lebesgue_measure.v`:
+  + `emeasurable_bigcup` -> `bigcupT_emeasurable`
+
+### Removed
+
+- files `posnum.v` and `nngnum.v` (both subsumed by `signed.v`)
+- in `topology.v`:
+  + `ltr_distlC`, `ler_distlC`
 
 ## [0.4.0] - 2022-03-08
 
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 21239e981..c1ee5bdc8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,63 +4,12 @@
 
 ### Added
 
-- in `signed.v`:
-  + notations `%:nngnum` and `%:posnum`
-- in `ereal.v`:
-  + notations `{posnum \bar R}` and `{nonneg \bar R}`
-  + notations `%:pos` and `%:nng` in `ereal_dual_scope` and `ereal_scope`
-  + variants `posnume_spec` and `nonnege_spec`
-  + definitions `posnume`, `nonnege`, `abse_reality_subdef`,
-    `ereal_sup_reality_subdef`, `ereal_inf_reality_subdef`
-  + lemmas `ereal_comparable`, `pinfty_snum_subproof`, `ninfty_snum_subproof`,
-    `EFin_snum_subproof`, `fine_snum_subproof`, `oppe_snum_subproof`,
-    `adde_snum_subproof`, `dadde_snum_subproof`, `mule_snum_subproof`,
-    `abse_reality_subdef`, `abse_snum_subproof`, `ereal_sup_snum_subproof`,
-    `ereal_inf_snum_subproof`, `num_abse_eq0`, `num_lee_maxr`, `num_lee_maxl`,
-    `num_lee_minr`, `num_lee_minl`, `num_lte_maxr`, `num_lte_maxl`,
-    `num_lte_minr`, `num_lte_minl`, `num_abs_le`, `num_abs_lt`,
-    `posnumeP`, `nonnegeP`
-  + signed instances `pinfty_snum`, `ninfty_snum`, `EFin_snum`, `fine_snum`,
-    `oppe_snum`, `adde_snum`, `dadde_snum`, `mule_snum`, `abse_snum`,
-    `ereal_sup_snum`, `ereal_inf_snum`
-
 ### Changed
 
-- in `functions.v`:
-  + `addrfunE` renamed to `addrfctE` and generalized to `Type`, `zmodType`
-  + `opprfunE` renamed to `opprfctE` and generalized to `Type`, `zmodType`
-- moved from `functions.v` to `classical_sets.v`
-  + lemma `subsetW`, definition `subsetCW`
-- in `mathcomp_extra.v`:
-  + fix notation `ltLHS`
-
 ### Renamed
 
-- in `topology.v`:
-  + `open_bigU` -> `bigcup_open`
-- in `functions.v`:
-  + `mulrfunE` -> `mulrfctE`
-  + `scalrfunE` -> `scalrfctE`
-  + `exprfunE` -> `exprfctE`
-  + `valLr` -> `valR`
-  + `valLr_fun` -> `valR_fun`
-  + `valLrK` -> `valRK`
-  + `oinv_valLr` -> `oinv_valR`
-  + `valLr_inj_subproof` -> `valR_inj_subproof`
-  + `valLr_surj_subproof` -> `valR_surj_subproof`
-- in `measure.v`:
-  + `measurable_bigcup` -> `bigcupT_measurable`
-  + `measurable_bigcap` -> `bigcapT_measurable`
-  + `measurable_bigcup_rat` -> `bigcupT_measurable_rat`
-- in `lebesgue_measure.v`:
-  + `emeasurable_bigcup` -> `bigcupT_emeasurable`
-
 ### Removed
 
-- files `posnum.v` and `nngnum.v` (both subsumed by `signed.v`)
-- in `topology.v`:
-  + `ltr_distlC`, `ler_distlC`
-
 ### Infrastructure
 
 ### Misc
diff --git a/INSTALL.md b/INSTALL.md
index 2523ca419..282cb5cad 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.4.0
+$ opam install coq-mathcomp-analysis.0.5.0
 ```
 4. Everytime you want to work in this same context, you need to type
 ```