Skip to content

Releases: damien-pous/coinduction

Coinduction 1.22, for Rocq 9.2

06 May 15:29

Choose a tag to compare

  • composition symbol (°) at level 40 to match other libs
  • removed warnings and deprecated symbols for rocq 9.2
  • formatting for `R notation
  • helpers for PreOrder, Equivalence, Proper1, Proper2

this version needs rocq 9.2 ;
in case notation changes cause problems, coinduction.1.22 also compiles with rocq 9.2

Coinduction 1.21, for Rocq 9.0

17 Sep 06:47

Choose a tag to compare

move from Coq to Rocq, transition packages no longer required

Coinduction 1.20, for Coq 8.20

18 Sep 08:59

Choose a tag to compare

compatibility release

Coinduction 1.9

18 Mar 09:30

Choose a tag to compare

  • 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

Coinduction 1.8

20 Oct 13:59

Choose a tag to compare

Better hint mode for typeclass CompleteLattice

Coinduction 1.7, tower-based, for Coq 8.16 and 8.17

13 Jul 13:45

Choose a tag to compare

  • 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

Coinduction 1.6, for Coq 8.16

08 Sep 15:43

Choose a tag to compare

compatibility with Coq 8.16

Coinduction 1.5, for Coq 8.15

30 Mar 11:00

Choose a tag to compare

compatibility with Coq 8.15

Coinduction 1.4, for Coq 8.14

30 Mar 08:24

Choose a tag to compare

  • add support for heterogeneous relations of arbitrary arity
  • only for coq 8.14 (lost compatibility with 8.13), release for 8.15 to arrive shortly

Coinduction 1.3, for Coq 8.13

29 Oct 18:36

Choose a tag to compare

Fix issue with slow unification problems occurring during typeclass resolution.