changelog for version 1.3.1

math-comp · Aug 9, 2024 · 579fdb4 · 579fdb4
1 parent 5517979
commit 579fdb4
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 3 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,6 +1,13 @@
 # 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
+
+### 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
@@ -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
@@ -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)