From 99c3a8336d2ca461f2766d18293cd26cbe4b1069 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 9 Aug 2024 23:55:21 +0900
Subject: [PATCH] changelog for version 1.3.1 (#1290)

* changelog for version 1.3.1
---
 CHANGELOG.md | 15 ++++++++++++++-
 INSTALL.md   |  2 +-
 README.md    |  2 +-
 3 files changed, 16 insertions(+), 3 deletions(-)

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)