v1.7 release (tower-based reimplementation)

CHANGELOG

@@ -1,15 +1,16 @@
-* 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
   (see changes in package coq-coinduction-examples)
   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
 

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