diff --git a/CHANGELOG b/CHANGELOG
index db29977..a93d31c 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,4 +1,4 @@
-* upcoming: v2.0
+* 13 Jul 2023: v1.7
 
 - tower-based reimplementation of the tactic
   not backward compatible, but required changes should only result in simplifications
@@ -6,10 +6,11 @@
   lemmas and definition related to the companion are kept in [companion.v]
 - library should be loaded with [From Coinduction Require Import all].
 - fixed efficiency issues with large arities
+- compatible with both Coq 8.16 and 8.17
 
 * 8 Sep. 2022: v1.6
 
-- compatibility with Coq 8.16
+- compatibility with Coq 8.16 (and 8.17)
 
 * 30 Mar. 2022: v1.5
 
diff --git a/README.md b/README.md
index 9159687..9d18f10 100644
--- a/README.md
+++ b/README.md
@@ -34,7 +34,6 @@ Examples on how to use the library may be found in the associated coq-coinductio
 - Coq-community maintainer(s):
   - Damien Pous ([**@damien-pous**](https://github.com/damien-pous))
 - License: [GNU LGPL3+]
-- Compatible Coq versions: 8.13 or later
 - Coq namespace: `Coinduction`
 - Related publication(s):
   - [Coinduction All the Way Up](https://hal.archives-ouvertes.fr/hal-01259622) doi:[10.1145/2933575.2934564](http://dx.doi.org/10.1145/2933575.2934564)
@@ -57,3 +56,9 @@ cd coinduction
 make
 make install
 ```
+
+## Compatibility
+
+- version v1.6 compiles with both Coq 8.16 and 8.17
+- so does version v1.7, which is feature equivalent but not backward-compatible with v1.6
+- the master branch of this git repository should compile with Coq master