Skip to content

AAC Tactics feature release for Coq 8.19

Compare
Choose a tag to compare
@palmskog palmskog released this 01 Jun 12:45
· 1 commit to v8.19 since this release
46abd8f

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.