diff --git a/CHANGELOG.md b/CHANGELOG.md
index c065ba76e..330b467c3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,93 @@
 # Changelog
 
-Last releases: [[0.3.3] - 2020-11-11](#033---2020-11-11) and [[0.3.2] - 2020-08-11](#032---2020-08-11)
+Last releases: [[0.3.4] - 2020-12-12](#034---2020-12-12) and [[0.3.3] - 2020-11-11](#033---2020-11-11)
+
+## [0.3.4] - 2020-12-12
+
+### Added
+
+- in `classical_sets.v`:
+  + lemma `bigcup_distrl`
+  + definition `trivIset`
+  + lemmas `trivIset_bigUI`, `trivIset_setI`
+- in `ereal.v`:
+  + definition `mule` and its notation `*` (scope `ereal_scope`)
+  + definition `abse` and its notation `` `| | `` (scope `ereal_scope`)
+- in `normedtype.v`:
+  + lemmas `closure_sup`, `near_infty_natSinv_lt`, `limit_pointP`
+  + lemmas `closure_gt`, `closure_lt`
+  + definition `is_interval`, `is_intervalPle`, `interval_is_interval`
+  + lemma `connected_intervalP`
+  + lemmas `interval_open` and `interval_closed`
+  + lemmas `inf_lb_strict`, `sup_ub_strict`, `interval_unbounded_setT`,
+    `right_bounded_interior`, `interval_left_unbounded_interior`, `left_bounded_interior`,
+    `interval_right_unbounded_interior`, `interval_bounded_interior`
+  + definition `Rhull`
+  + lemma `sub_Rhull`, `is_intervalP`
+- in `measure.v`:
+  + definition `bigcup2`, lemma `bigcup2E`
+  + definitions `isSemiRingOfSets`, `SemiRingOfSets`, notation `semiRingOfSetsType`
+  + definitions `RingOfSets_from_semiRingOfSets`, `RingOfSets`, notation `ringOfSetsType`
+  + factory: `isRingOfSets`
+  + definitions `Measurable_from_ringOfSets`, `Measurable`
+  + lemma `semiRingOfSets_measurable{I,D}`
+  + definition `diff_fsets`, lemmas `semiRingOfSets_diff_fsetsE`, `semiRingOfSets_diff_fsets_disjoint`
+  + definitions `isMeasurable`
+  + factory: `isMeasurable`
+  + lemma `bigsetU_measurable`, `measurable_bigcap`
+  + definitions `semi_additive2`, `semi_additive`, `semi_sigma_additive`
+  + lemmas `semi_additive2P`, `semi_additiveE`, `semi_additive2E`,
+    `semi_sigma_additive_is_additive`, `semi_sigma_additiveE`
+  + `Module AdditiveMeasure`
+     * notations `additive_measure`, `{additive_measure set T -> {ereal R}}`
+  + lemmas `measure_semi_additive2`, `measure_semi_additive`, `measure_semi_sigma_additive`
+  + lemma `semi_sigma_additive_is_additive`, canonical/coercion `measure_additive_measure`
+  + lemma `sigma_additive_is_additive`
+  + notations `ringOfSetsType`, `outer_measure`
+  + definition `negligible` and its notation `.-negligible`
+  + lemmas `negligibleP`, `negligible_set0`
+  + definition `almost_everywhere` and its notation `{ae mu, P}`
+  + lemma `satisfied_almost_everywhere`
+  + definition `sigma_subadditive`
+  + `Module OuterMeasure`
+    * notation `outer_measure`, `{outer_measure set T -> {ereal R}}`
+  + lemmas `outer_measure0`, `outer_measure_ge0`, `le_outer_measure`,
+    `outer_measure_sigma_subadditive`, `le_outer_measureIC`
+- in `boolp.v`:
+  + lemmas `and3_asboolP`, `or3_asboolP`, `not_and3P`
+- in `classical_sets.v`:
+  + lemma `bigcup_sup`
+- in `topology.v`:
+  + lemmas `closure0`, `separatedC`, `separated_disjoint`, `connectedP`, `connected_subset`,
+    `bigcup_connected`
+  + definition `connected_component`
+  + lemma `component_connected`
+
+### Changed
+
+- in `ereal.v`:
+  + notation `x >= y` defined as `y <= x` (only parsing) instead of `gee`
+  + notation `x > y` defined as `y < x` (only parsing) instead of `gte`
+  + definition `mkset`
+  + lemma `eq_set`
+- in `classical_sets.v`:
+  + notation `[set x : T | P]` now use definition `mkset`
+- in `reals.v`:
+  + lemmas generalized from `realType` to `numDomainType`:
+    `setNK`, `memNE`, `lb_ubN`, `ub_lbN`, `nonemptyN`, `has_lb_ubN `
+  + lemmas generalized from `realType` to `realDomainType`:
+    `has_ubPn`, `has_lbPn`
+
+## Renamed
+
+- in `classical_sets.v`:
+  + `subset_empty` -> `subset_nonempty`
+- in `measure.v`:
+  + `sigma_additive_implies_additive` -> `sigma_additive_is_additive`
+- in `topology.v`:
+  + `nbhs_of` -> `locally_of`
+- in `topology.v`:
+  + `connect0` -> `connected0`
 
 ## [0.3.3] - 2020-11-11
 
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 5c96510d7..c1ee5bdc8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,89 +4,10 @@
 
 ### Added
 
-- in `classical_sets.v`:
-  + lemma `bigcup_distrl`
-  + definition `trivIset`
-  + lemmas `trivIset_bigUI`, `trivIset_setI`
-- in `ereal.v`:
-  + definition `mule` and its notation `*` (scope `ereal_scope`)
-  + definition `abse` and its notation `` `| | `` (scope `ereal_scope`)
-- in `normedtype.v`:
-  + lemmas `closure_sup`, `near_infty_natSinv_lt`, `limit_pointP`
-  + lemmas `closure_gt`, `closure_lt`
-  + definition `is_interval`, `is_intervalPle`, `interval_is_interval`
-  + lemma `connected_intervalP`
-  + lemmas `interval_open` and `interval_closed`
-  + lemmas `inf_lb_strict`, `sup_ub_strict`, `interval_unbounded_setT`,
-    `right_bounded_interior`, `interval_left_unbounded_interior`, `left_bounded_interior`,
-    `interval_right_unbounded_interior`, `interval_bounded_interior`
-  + definition `Rhull`
-  + lemma `sub_Rhull`, `is_intervalP`
-- in `measure.v`:
-  + definition `bigcup2`, lemma `bigcup2E`
-  + definitions `isSemiRingOfSets`, `SemiRingOfSets`, notation `semiRingOfSetsType`
-  + definitions `RingOfSets_from_semiRingOfSets`, `RingOfSets`, notation `ringOfSetsType`
-  + factory: `isRingOfSets`
-  + definitions `Measurable_from_ringOfSets`, `Measurable`
-  + lemma `semiRingOfSets_measurable{I,D}`
-  + definition `diff_fsets`, lemmas `semiRingOfSets_diff_fsetsE`, `semiRingOfSets_diff_fsets_disjoint`
-  + definitions `isMeasurable`
-  + factory: `isMeasurable`
-  + lemma `bigsetU_measurable`, `measurable_bigcap`
-  + definitions `semi_additive2`, `semi_additive`, `semi_sigma_additive`
-  + lemmas `semi_additive2P`, `semi_additiveE`, `semi_additive2E`,
-    `semi_sigma_additive_is_additive`, `semi_sigma_additiveE`
-  + `Module AdditiveMeasure`
-     * notations `additive_measure`, `{additive_measure set T -> {ereal R}}`
-  + lemmas `measure_semi_additive2`, `measure_semi_additive`, `measure_semi_sigma_additive`
-  + lemma `semi_sigma_additive_is_additive`, canonical/coercion `measure_additive_measure`
-  + lemma `sigma_additive_is_additive`
-  + notations `ringOfSetsType`, `outer_measure`
-  + definition `negligible` and its notation `.-negligible`
-  + lemmas `negligibleP`, `negligible_set0`
-  + definition `almost_everywhere` and its notation `{ae mu, P}`
-  + lemma `satisfied_almost_everywhere`
-  + definition `sigma_subadditive`
-  + `Module OuterMeasure`
-    * notation `outer_measure`, `{outer_measure set T -> {ereal R}}`
-  + lemmas `outer_measure0`, `outer_measure_ge0`, `le_outer_measure`,
-    `outer_measure_sigma_subadditive`, `le_outer_measureIC`
-- in `boolp.v`:
-  + lemmas `and3_asboolP`, `or3_asboolP`, `not_and3P`
-- in `classical_sets.v`:
-  + lemma `bigcup_sup`
-- in `topology.v`:
-  + lemmas `closure0`, `separatedC`, `separated_disjoint`, `connectedP`, `connected_subset`,
-    `bigcup_connected`
-  + definition `connected_component`
-  + lemma `component_connected`
-
 ### Changed
 
-- in `ereal.v`:
-  + notation `x >= y` defined as `y <= x` (only parsing) instead of `gee`
-  + notation `x > y` defined as `y < x` (only parsing) instead of `gte`
-  + definition `mkset`
-  + lemma `eq_set`
-- in `classical_sets.v`:
-  + notation `[set x : T | P]` now use definition `mkset`
-- in `reals.v`:
-  + lemmas generalized from `realType` to `numDomainType`:
-    `setNK`, `memNE`, `lb_ubN`, `ub_lbN`, `nonemptyN`, `has_lb_ubN `
-  + lemmas generalized from `realType` to `realDomainType`:
-    `has_ubPn`, `has_lbPn`
-
 ### Renamed
 
-- in `classical_sets.v`:
-  + `subset_empty` -> `subset_nonempty`
-- in `measure.v`:
-  + `sigma_additive_implies_additive` -> `sigma_additive_is_additive`
-- in `topology.v`:
-  + `nbhs_of` -> `locally_of`
-- in `topology.v`:
-  + `connect0` -> `connected0`
-
 ### Removed
 
 ### Infrastructure
diff --git a/INSTALL.md b/INSTALL.md
index e277333af..a3945bce7 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -1,8 +1,9 @@
 # Installing
 
 ## Requirements
-- [The Coq Proof Assistant version ≥ 8.10](https://coq.inria.fr)
-- [Mathematical Components version ≥ 1.11.0](https://github.com/math-comp/math-comp)
+
+- [The Coq Proof Assistant version ≥ 8.11](https://coq.inria.fr)
+- [Mathematical Components version = 1.11.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 1.5.0](https://github.com/math-comp/finmap)
 
 These requirements can be installed in a custom way, or through
@@ -14,13 +15,14 @@ Detailed instructions for possible installations of Mathematical Components are
 [here](https://github.com/math-comp/math-comp/blob/master/INSTALL.md).
 
 ## Short Instructions
+
 - Through opam:
   + type `opam install coq-mathcomp-analysis.X.Y.Z` where `X.Y.Z` is the version number
     (all the dependencies should be automatically installed, assuming `opam` has been properly
     configured and `coq-released` repository is added)
-- Custom (assuming Coq ≥ 8.10, Mathematical Components version ≥ 1.11.0, and Finmap version ≥ 1.5.0
-  have been installed):
-  + Type `make` to use the provided `Makefile`.
+- Custom (assuming Coq ≥ 8.11, Mathematical Components version = 1.11.0, Finmap version ≥ 1.5.0,
+  and Hierarchy Builder ≥ 0.10.0 have been installed):
+  + type `make` to use the provided `Makefile`
 
 ## From scratch instructions
 
@@ -45,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.3.3
+$ opam install coq-mathcomp-analysis.0.3.4
 ```
 4. Everytime you want to work in this same context, you need to type
 ```
@@ -75,26 +77,31 @@ version numbers accordingly.
 ```
 $ opam install coq.8.12.0
 ```
-2. Install Mathematical Components development version 
+2. Install the Mathematical Components
 ```
 $ opam install coq-mathcomp-ssreflect.1.11.0
 $ opam install coq-mathcomp-fingroup.1.11.0
 $ opam install coq-mathcomp-algebra.1.11.0
 $ opam install coq-mathcomp-solvable.1.11.0
 $ opam install coq-mathcomp-field.1.11.0
-$ opam install coq-mathcomp-bigenough.1.0.0
 ```
-3. Install Finite maps library
+3. Install the Finite maps library
 ```
 $ opam install coq-mathcomp-finmap.1.5.0
 ```
-4. Download and compile `coq-mathcomp-analysis` without installing
+4. Install the Hierarchy Builder
+```
+$ opam install coq-hierarchy-builder.0.10.0
+```
+5. Download and compile `coq-mathcomp-analysis` without installing
 ```
 $ git clone https://github.com/math-comp/analysis
 $ cd analysis
 $ make
 ```
+
 ## How to clean your computer
+
 - If you installed the package `coq-mathcomp-analysis` and wish to get rid of it, just type
 ```
 $ opam remove coq-mathcomp-analysis