Releases: coq-community/aac-tactics
Releases · coq-community/aac-tactics
AAC Tactics release for Coq 8.20
AAC Tactics feature release for Coq 8.19
Release with Coq 8.19 compatibility.
Added
aac_normalise in H
tactic.gcd
andlcm
instances forNat
,N
, andZ
.
Fixed
- Make the order of sums produced by
aac_normalise
tactic consistent across calls.
AAC Tactics release for Coq 8.19
Release with Coq 8.19 compatibility.
AAC Tactics release for Coq 8.18
Release with Coq 8.18 compatibility.
AAC Tactics release for Coq 8.17
Release with Coq 8.17 and OCaml 5 compatibility.
AAC Tactics release for Coq 8.16
Release with Coq 8.16 compatibility.
AAC Tactics bugfix release for Coq 8.15
Release with 8.15 compatibility that fixes a universe typing issue which prevented some reasoning AAC with relations on parameterized structures such as lists. Also adds permutation typeclass instances and switches to export locality for typeclass instances whenever possible.
AAC Tactics release for Coq 8.15
Release with Coq 8.15 compatibility.
AAC Tactics feature release for Coq 8.14
Release with Coq 8.14 compatibility that adds support for simplification based on idempotence of commutative operators.
AAC Tactics feature release for Coq 8.13
Release with Coq 8.13 compatibility that adds support for simplification based on idempotence of commutative operators.