CHANGELOG

* 18 Sep 2024: v1.20

- compatibility with Coq 8.20

* 18 Mar 2024: v1.9

- compatibility with Coq 8.19
- linking the companion to the tower as defined in [tower.v]
- monotonicity of [gfp] and related lemmas for the chain and the companion

* 20 OCt 2023: v1.8

- compatibility with Coq 8.18
- hint mode for typeclass CompleteLattice to avoid divergences

* 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 (and 8.17)

* 30 Mar. 2022: v1.5

- compatibility with Coq 8.15

* 30 Mar. 2022: v1.4

- tactic support for heterogeneous relations of arbitrary and possibly dependent arity
  (cf. https://github.com/damien-pous/coinduction/issues/5)

* 29 Oct. 2021: v1.3

- declare some values (t,B,T) as opaque and opaque for typeclasses
  in order to avoid efficiency issues with unification
  (cf. https://github.com/damien-pous/coinduction/issues/2)

* 8 Oct. 2021: v1.2

- fixes handling of universes constraints in OCaml plugin
- new helpers for proving that contextual functions are below the companion