changelog for version 1.3.1

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
 

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
 ```

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)