AAC Tactics Release for Rocq 9.0

Release with Rocq 9.0 compatibility.

AAC Tactics release for Coq 8.20

Release with Coq 8.20 compatibility.

Added

• Tests for try aac_rewrite and try aac_normalise that failed on 8.19

AAC Tactics feature release for Coq 8.19

Release with Coq 8.19 compatibility.

Added

• aac_normalise in H tactic.
• gcd and lcm instances for Nat, N, and Z.

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.