Skip to content

Releases: coq-community/aac-tactics

AAC Tactics release for Coq 8.20

27 Jun 19:52
Compare
Choose a tag to compare

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

01 Jun 12:45
46abd8f
Compare
Choose a tag to compare

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

22 Dec 11:04
Compare
Choose a tag to compare

Release with Coq 8.19 compatibility.

AAC Tactics release for Coq 8.18

04 Aug 07:20
Compare
Choose a tag to compare

Release with Coq 8.18 compatibility.

AAC Tactics release for Coq 8.17

30 Dec 02:22
Compare
Choose a tag to compare

Release with Coq 8.17 and OCaml 5 compatibility.

AAC Tactics release for Coq 8.16

18 Jun 12:50
Compare
Choose a tag to compare

Release with Coq 8.16 compatibility.

AAC Tactics bugfix release for Coq 8.15

15 Mar 20:17
45af31f
Compare
Choose a tag to compare

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

11 Dec 14:39
Compare
Choose a tag to compare

Release with Coq 8.15 compatibility.

AAC Tactics feature release for Coq 8.14

10 Oct 10:00
Compare
Choose a tag to compare

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

10 Oct 09:58
9f4c897
Compare
Choose a tag to compare

Release with Coq 8.13 compatibility that adds support for simplification based on idempotence of commutative operators.