diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4a5b57ca1..62d5ebc18 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,96 @@
 # Changelog
 
-Lastest releases: [[0.5.3] - 2022-08-10](#053---2022-08-10) and [[0.5.2] - 2022-06-08](#052---2022-07-08)
+Lastest releases: [[0.5.4] - 2022-09-07](#055---2022-09-07) and [[0.5.3] - 2022-08-10](#053---2022-08-10)
+
+## [0.5.4] - 2022-09-07
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + defintion `onem` and notation ``` `1- ```
+  + lemmas `onem0`, `onem1`, `onemK`, `onem_gt0`, `onem_ge0`, `onem_le1`, `onem_lt1`,
+    `onemX_ge0`, `onemX_lt1`, `onemD`, `onemMr`, `onemM`
+  + lemmas `natr1`, `nat1r`
+- in `classical_sets.v`:
+  + lemmas `subset_fst_set`, `subset_snd_set`, `fst_set_fst`, `snd_set_snd`,
+    `fset_setM`, `snd_setM`, `fst_setMR`
+  + lemmas `xsection_snd_set`, `ysection_fst_set`
+- in `constructive_ereal.v`:
+  + lemmas `ltNye_eq`, `sube_lt0`, `subre_lt0`, `suber_lt0`, `sube_ge0`
+  + lemmas `dsubre_gt0`, `dsuber_gt0`, `dsube_gt0`, `dsube_le0`
+- in `signed.v`:
+  + lemmas `onem_PosNum`, `onemX_NngNum`
+- in `fsbigop.v`:
+  + lemmas `lee_fsum_nneg_subset`, `lee_fsum`
+- in `topology.v`:
+  + lemma `near_inftyS`
+  + lemma `continuous_closedP`, `closedU`, `pasting`
+  + lemma `continuous_inP`
+  + lemmas `open_setIS`, `open_setSI`, `closed_setIS`, `closed_setSI`
+- in `normedtype.v`:
+  + definitions `contraction` and `is_contraction`
+  + lemma `contraction_fixpoint_unique`
+- in `sequences.v`:
+  + lemmas `contraction_dist`, `contraction_cvg`,
+    `contraction_cvg_fixed`, `banach_fixed_point`,
+    `contraction_unique`
+- in `derive.v`:
+  + lemma `diff_derivable`
+- in `measure.v`:
+  + lemma `measurable_funTS`
+- in `lebesgue_measure.v`:
+  + lemma `measurable_fun_fine`
+  + lemma `open_measurable_subspace`
+  + lemma ``subspace_continuous_measurable_fun``
+  + corollary `open_continuous_measurable_fun`
+  + Hint about `measurable_fun_normr`
+- in `lebesgue_integral.v`:
+  + lemma `measurable_fun_indic`
+  + lemma `ge0_integral_mscale`
+  + lemma `integral_pushforward`
+
+### Changed
+
+- in `esum.v`:
+  + definition `esum`
+- moved from `lebesgue_integral.v` to `classical_sets.v`:
+  + `mem_set_pair1` -> `mem_xsection`
+  + `mem_set_pair2` -> `mem_ysection`
+- in `derive.v`:
+  + generalized `is_diff_scalel`
+- in `measure.v`:
+  + generalize `measurable_uncurry`
+- in `lebesgue_measure.v`:
+  + `pushforward` requires a proof that its argument is measurable
+- in `lebesgue_integral.v`:
+  + change implicits of `integralM_indic`
+
+### Renamed
+
+- in `constructive_ereal.v`:
+  + `lte_pinfty_eq` -> `ltey_eq`
+  + `le0R` -> `fine_ge0`
+  + `lt0R` -> `fine_gt0`
+- in `ereal.v`:
+  + `lee_pinfty_eq` -> `leye_eq`
+  + `lee_ninfty_eq` -> `leeNy_eq`
+- in `esum.v`:
+  + `esum0` -> `esum1`
+- in `sequences.v`:
+  + `nneseries_lim_ge0` -> `nneseries_ge0`
+- in `measure.v`:
+  + `ring_fsets` -> `ring_finite_set`
+  + `discrete_measurable` -> `discrete_measurable_nat`
+  + `cvg_mu_inc` -> `nondecreasing_cvg_mu`
+- in `lebesgue_integral.v`:
+  + `muleindic_ge0` -> `nnfun_muleindic_ge0`
+  + `mulem_ge0` -> `mulemu_ge0`
+  + `nnfun_mulem_ge0` -> `nnsfun_mulemu_ge0`
+
+### Removed
+
+- in `esum.v`:
+  + lemma `fsetsP`, `sum_fset_set`
 
 ## [0.5.3] - 2022-08-10
 
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 1e13dea62..c1ee5bdc8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -3,104 +3,13 @@
 ## [Unreleased]
 
 ### Added
-- in `normedtype.v`:
-  + definitions `contraction` and `is_contraction`
-  + lemma `contraction_fixpoint_unique`
-
-- in `constructive_ereal.v`:
-  + lemmas `ltNye_eq`, `sube_lt0`, `subre_lt0`, `suber_lt0`, `sube_ge0`
-  + lemmas `dsubre_gt0`, `dsuber_gt0`, `dsube_gt0`, `dsube_le0`
-
-- in `topology.v`:
-  + lemma `near_inftyS`
-  + lemma `continuous_closedP`, `closedU`, `pasting`
-
-- in `sequences.v`:
-  + lemmas `contraction_dist`, `contraction_cvg`,
-    `contraction_cvg_fixed`, `banach_fixed_point`,
-    `contraction_unique`
-- in `mathcomp_extra.v`:
-  + defintion `onem` and notation ``` `1- ```
-  + lemmas `onem0`, `onem1`, `onemK`, `onem_gt0`, `onem_ge0`, `onem_le1`, `onem_lt1`,
-    `onemX_ge0`, `onemX_lt1`, `onemD`, `onemMr`, `onemM`
-- in `signed.v`:
-  + lemmas `onem_PosNum`, `onemX_NngNum`
-- in `lebesgue_measure.v`:
-  + lemma `measurable_fun_fine`
-- in `lebesgue_integral.v`:
-  + lemma `ge0_integral_mscale`
-- in `measure.v`:
-  + lemma `measurable_funTS`
-- in `lebesgue_measure.v`:
-  + lemma `measurable_fun_indic`
-- in `fsbigop.v`:
-  + lemmas `lee_fsum_nneg_subset`, `lee_fsum`
-- in `classical_sets.v`:
-  + lemmas `subset_fst_set`, `subset_snd_set`, `fst_set_fst`, `snd_set_snd`,
-    `fset_setM`, `snd_setM`, `fst_setMR`
-  + lemmas `xsection_snd_set`, `ysection_fst_set`
-  + Hint about `measurable_fun_normr`
-- in `lebesgue_integral.v`:
-  + lemma `integral_pushforward`
-
-- in `derive.v`:
-  + lemma `diff_derivable`
-- in `topology.v`:
-  + lemma `continuous_inP`
-- in `lebesgue_measure.v`:
-  + lemma `open_measurable_subspace`
-  + lemma ``subspace_continuous_measurable_fun``
-  + corollary `open_continuous_measurable_fun`
-- in `topology.v`:
-  + lemmas `open_setIS`, `open_setSI`, `closed_setIS`, `closed_setSI`
-- in `mathcomp_extra.v`:
-  + lemmas `natr1`, `nat1r`
 
 ### Changed
 
-- in `measure.v`:
-  + generalize `measurable_uncurry`
-- in `esum.v`:
-  + definition `esum`
-- moved from `lebesgue_integral.v` to `classical_sets.v`:
-  + `mem_set_pair1` -> `mem_xsection`
-  + `mem_set_pair2` -> `mem_ysection`
-- in `lebesgue_measure.v`:
-  + `pushforward` requires a proof that its argument is measurable
-- in `lebesgue_integral.v`:
-  + change implicits of `integralM_indic`
-- in `derive.v`:
-  + generalized `is_diff_scalel`
-
 ### Renamed
 
-- in `constructive_ereal.v`:
-  + `lte_pinfty_eq` -> `ltey_eq`
-- in `sequences.v`:
-  + `nneseries_lim_ge0` -> `nneseries_ge0`
-- in `constructive_ereal.v`:
-  + `le0R` -> `fine_ge0`
-  + `lt0R` -> `fine_gt0`
-- in `measure.v`:
-  + `ring_fsets` -> `ring_finite_set`
-  + `discrete_measurable` -> `discrete_measurable_nat`
-- in `ereal.v`:
-  + `lee_pinfty_eq` -> `leye_eq`
-  + `lee_ninfty_eq` -> `leeNy_eq`
-- in `measure.v`:
-  + `cvg_mu_inc` -> `nondecreasing_cvg_mu`
-- in `lebesgue_integral.v`:
-  + `muleindic_ge0` -> `nnfun_muleindic_ge0`
-  + `mulem_ge0` -> `mulemu_ge0`
-  + `nnfun_mulem_ge0` -> `nnsfun_mulemu_ge0`
-- in `esum.v`:
-  + `esum0` -> `esum1`
-
 ### Removed
 
-- in `esum.v`:
-  + lemma `fsetsP`, `sum_fset_set`
-
 ### Infrastructure
 
 ### Misc
diff --git a/INSTALL.md b/INSTALL.md
index 5b0c85aac..19435cf87 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -5,7 +5,7 @@
 - [The Coq Proof Assistant version ≥ 8.13](https://coq.inria.fr)
 - [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
-- [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder)
+- [Hierarchy builder version >= 1.3.0](https://github.com/math-comp/hierarchy-builder)
 
 These requirements can be installed in a custom way, or through
 [opam](https://opam.ocaml.org/) (the recommended way) using
@@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.5.3
+$ opam install coq-mathcomp-analysis.0.5.4
 ```
 4. Everytime you want to work in this same context, you need to type
 ```
diff --git a/README.md b/README.md
index 723f921bc..c7748564f 100644
--- a/README.md
+++ b/README.md
@@ -33,7 +33,7 @@ the Coq proof-assistant and using the Mathematical Components library.
   - Pierre-Yves Strub (initial)
   - Laurent Théry
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: Coq 8.14 to 8.15 (or dev)
+- Compatible Coq versions: Coq 8.14 to 8.16 (or dev)
 - Additional dependencies:
   - [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
   - [MathComp fingroup 1.13 or later](https://math-comp.github.io)
diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam
index dacb81fa1..3e8ca66e9 100644
--- a/coq-mathcomp-analysis.opam
+++ b/coq-mathcomp-analysis.opam
@@ -18,7 +18,7 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.14" & < "8.16~") | (= "dev") }
+  "coq" { (>= "8.14" & < "8.17~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev") }
   "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.16~") | (= "dev") }
   "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.16~") | (= "dev") }
diff --git a/meta.yml b/meta.yml
index 9690e63d3..9223c2079 100644
--- a/meta.yml
+++ b/meta.yml
@@ -49,8 +49,8 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.14 to 8.15 (or dev)
-  opam: '{ (>= "8.14" & < "8.16~") | (= "dev") }'
+  text: Coq 8.14 to 8.16 (or dev)
+  opam: '{ (>= "8.14" & < "8.17~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '1.13.0-coq-8.14'