Skip to content

Algebra Tactics 1.2.0
Compare
Choose a tag to compare
@pi8027 pi8027 released this 28 Sep 13:28
· 33 commits to master since this release
1.2.0
b8a2149
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Verified
Learn about vigilant mode.

This release is compatible with Coq 8.16 to 8.18, MathComp 2.0, Mczify 1.15, and Coq-Elpi 1.15 to 1.19 (except 1.17.0).

  • The ring tactic now supports commutative semirings as in the ring tactic of Coq, thanks to the semiRingType and comSemiRingType structures introduced in MathComp 2.0. All the provided tactics support semiring homomorphisms applied to semiring subexpressions as well.
  • The lra, nra, and psatz tactics now support additive functions applied to Z-module or N-module subexpressions.
  • The preprocessors now automatically compress homomorphisms from "initial objects" (nat, N, int, and Z) to the canonical ones (e.g., intr) and thus equate more variables.

EDIT: the ring tactic actually does not work for commutative semirings. This issue will be fixed in Algebra Tactics 1.2.1.

Assets 2
Loading