Skip to content

Algebra Tactics 1.0.0
Compare
Choose a tag to compare
@pi8027 pi8027 released this 25 Apr 16:10
· 80 commits to master since this release
1.0.0
a2edba0
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

This is the first stable release of Algebra Tactics, compatible with Coq 8.13 to 8.15, MathComp 1.12 to 1.14, Mczify 1.1 to 1.2, and Coq-Elpi 1.10.1 to 1.14.

  • The provided tactics now report time spent for reification and reflection only when the #[verbose] attribute is supplied.
  • The ring and field tactics do not accept implications as goals anymore. To reason modulo monomial equalities, the equalities have to be explicitly provided as arguments, e.g., ring: Ha Hb.
Assets 2
Loading