Skip to content

AAC Tactics feature release for Coq 8.19

Choose a tag to compare

View all tags
@palmskog palmskog released this 01 Jun 12:45
· 1 commit to v8.19 since this release
v8.19.1
46abd8f
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

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.
Assets 3
Loading