diff --git a/CHANGELOG.md b/CHANGELOG.md
index 22c7d3fd5..77e7ac33c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,19 @@
 # Changelog
 
-Latest releases: [[1.3.0] - 2024-08-06](#130---2024-08-06) and [[1.2.0] - 2024-06-06](#120---2024-06-06)
+Latest releases: [[1.3.1] - 2024-08-09](#131---2024-08-09) and [[1.3.0] - 2024-08-06](#130---2024-08-06)
+
+## [1.3.1] - 2024-08-09
+
+### Changed
+
+- in `wochoice.v`:
+  + two applications of the lemma `in3W` have been removed because they seem to cause
+    a universe inconsistency when one loads the `ring` module of `algebra-tactics`
+
+### Generalized
+
+- in `reals.v`:
+  + lemma `rat_in_itvoo` (from `realType` to `archiFieldType`)
 
 ## [1.3.0] - 2024-08-06
 
diff --git a/INSTALL.md b/INSTALL.md
index 4114dd836..0baa06422 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -48,7 +48,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.1.3.0
+$ opam install coq-mathcomp-analysis.1.3.1
 ```
 4. Everytime you want to work in this same context, you need to type
 ```
diff --git a/README.md b/README.md
index bee53eeb3..6ddf95d55 100644
--- a/README.md
+++ b/README.md
@@ -83,7 +83,7 @@ We try to preserve backward compatibility as best as we can.
 ## Documentation
 
 Each file is documented in its header
-([documentation for the last version](https://math-comp.github.io/analysis/htmldoc_1_3_0/index.html), using [`coq2html`](https://github.com/xavierleroy/coq2html)).
+([documentation for the last version](https://math-comp.github.io/analysis/htmldoc_1_3_1/index.html), using [`coq2html`](https://github.com/xavierleroy/coq2html)).
 
 Overview presentations:
 - [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)