diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 000000000..0f1af3f97
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,17 @@
+# Changelog
+
+## [0.3.0] - 2020-05-??
+
+This release is compatible with MathComp version 1.11.0+beta1
+
+### Added
+
+### Changed
+
+### Renamed
+
+### Removed
+
+### Infrastructure
+
+### Misc
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
new file mode 100644
index 000000000..616187d7e
--- /dev/null
+++ b/CHANGELOG_UNRELEASED.md
@@ -0,0 +1,85 @@
+# Changelog (unreleased)
+
+## [Unreleased]
+
+The biggest change of this release is compatibility with MathComp
+1.11.0.  The latter introduces in particular ordered types. The
+notation for the norm is now uniform.
+
+### Added
+
+- `sequences.v`: Main theorems about sequences and series, and examples
+  + Definitions:
+    * `[sequence E]_n` is a special notation for `fun n => E`
+    * `series u_` is the sequence of partial sums
+    * `[normed S]` is the series of absolute values, if S is a series
+    * `harmonic` is the name of a sequence,
+       apply `series` to them to get the series.
+  + Theorems:
+    * lots of helper lemmas to prove convergence of sequences
+    * convergence of harmonic sequence
+    * convergence of a series implies convergence of a sequence
+    * absolute convergence implies convergence of series
+- in `ereal.v`: lemmas about extended reals' arithmetic
+- in `normedtype.v`: Definitions and lemmas about generic domination,
+  boundedness, and lipschitz
+  + See header for the notations and their localization
+  + Added a bunch of combinators to extract existential witnesses
+  + Added `filter_forall` (commutation between a filter and finite forall)
+- about extended reals:
+  + equip extended reals with a structure of topological space
+  + show that extended reals are hausdorff
+- in `topology.v`, predicate `close`
+- lemmas about bigmaxr and argmaxr
+  + `\big[max/x]_P F = F [arg max_P F]`
+  + similar lemma for `bigmin`
+- lemmas for `within`
+- add `setICl` (intersection of set with its complement)
+- `prodnormedzmodule.v`
+  + `ProdNormedZmodule` transfered from MathComp
+  + `nonneg` type for non-negative numbers
+- `bigmaxr`/`bigminr` library
+- Lemmas `interiorI`, `setCU` (complement of union is intersection of complements),
+  `setICl`, `nonsubset`, `setC0`, `setCK`, `setCT`, `preimage_setI/U`, lemmas about `image`
+
+### Changed
+
+- in `Rstruct.v`, `bigmaxr` is now defined using `bigop`
+- `inE` now supports `in_setE` and `in_fsetE`
+- fix the definition of `le_ereal`, `lt_ereal`
+- various generalizations to better use the hierarchy of `ssrnum` (`numDomainType`,
+  `numFieldType`, `realDomainType`, etc. when possible) in `topology.v`,
+  `normedtype.v`, `derive.v`, etc.
+
+### Renamed
+
+- big refactoring about naming conventions
+  + complete the theory of `cvg_`, `is_cvg_` and `lim_` in normedtype.v
+    with consistent naming schemes
+  + fixed differential of `inv` which was defined on `1 / x` instead of `x^-1`
+  + two versions of lemmas on inverse exist
+    * one in realType (`Rinv_` lemmas), for which we have differential
+    * one in numClosedFieldType (no differential so far, just continuity)
+  + renamed `cvg_norm` to `cvg_dist` to reuse the name `cvg_norm` for
+    convergence under the norm
+- rename `is_prop` to `is_subset1`
+- renaming `flim` to `cvg`
+  + `cvg` corresponds to `_ --> _`
+  + `lim` corresponds to `lim _`
+  + `continuous`  corresponds to continuity
+  + some suffixes `_opp`, `_add` ... renamed to `N`, `D`, ...
+- `Uniform` renamed to `PseudoMetric`
+
+### Removed
+
+- `sub_trans` (replaced by MathComp's `subrKA`)
+- `derive.v` does not require `Reals` anymore
+- `Rbar.v` is almost not used anymore
+
+### Infrastructure
+
+- NIX support
+  + see `config.nix`, `default.nix`
+  + for the CI also
+
+### Misc