diff --git a/CHANGELOG.md b/CHANGELOG.md
index 330b467c3..9548a9504 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,34 @@
 # Changelog
 
-Last releases: [[0.3.4] - 2020-12-12](#034---2020-12-12) and [[0.3.3] - 2020-11-11](#033---2020-11-11)
+Last releases: [[0.3.5] - 2020-12-21](#035---2020-12-21) and [[0.3.4] - 2020-12-12](#034---2020-12-12)
+
+## [0.3.5] - 2020-12-21
+
+### Added
+
+- in `classical_sets.v`:
+  + lemmas `predeqP`, `seteqP`
+
+### Changed
+
+- Requires:
+  + MathComp >= 1.12
+- in `boolp.v`:
+  + lemmas `contra_not`, `contra_notT`, `contra_notN`, `contra_not_neq`, `contraPnot`
+    are now provided by MathComp 1.12
+- in `normedtype.v`:
+  + lemmas `ltr_distW`, `ler_distW` are now provided by MathComp 1.12 as lemmas
+    `ltr_distlC_subl` and `ler_distl_subl`
+  + lemmas `maxr_real` and `bigmaxr_real` are now provided by MathComp 1.12 as
+    lemmas `max_real` and `bigmax_real`
+  + definitions `isBOpen` and `isBClosed` are replaced by the definition `bound_side`
+  + definition `Rhull` now uses `BSide` instead of `BOpen_if`
+
+### Removed
+
+- Drop support for MathComp 1.11
+- in `topology.v`:
+  + `Typeclasses Opaque fmap.`
 
 ## [0.3.4] - 2020-12-12
 
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3e1106834..c1ee5bdc8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,31 +4,12 @@
 
 ### Added
 
-- in `classical_sets.v`:
-  + lemmas `predeqP`, `seteqP`
-
 ### Changed
 
-- Requires:
-  + MathComp >= 1.12
-- in `boolp.v`:
-  + lemmas `contra_not`, `contra_notT`, `contra_notN`, `contra_not_neq`, `contraPnot`
-    are now provided by MathComp 1.12
-- in `normedtype.v`:
-  + lemmas `ltr_distW`, `ler_distW` are now provided by MathComp 1.12 as lemmas
-    `ltr_distlC_subl` and `ler_distl_subl`
-  + lemmas `maxr_real` and `bigmaxr_real` are now provided by MathComp 1.12 as
-    lemmas `max_real` and `bigmax_real`
-  + definitions `isBOpen` and `isBClosed` are replaced by the definition `bound_side`
-  + definition `Rhull` now uses `BSide` instead of `BOpen_if`
-
 ### Renamed
 
 ### Removed
 
-- Drop support for MathComp 1.11
-- Typeclasses Opaque fmap.
-
 ### Infrastructure
 
 ### Misc