Skip to content

Algebra Tactics 1.1.0
Compare
Choose a tag to compare
@pi8027 pi8027 released this 29 Mar 13:40
· 45 commits to master since this release
1.1.0
edc8e5e
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 release is compatible with Coq 8.16 to 8.17, MathComp 1.15 to 1.16, Mczify 1.1 to 1.3, and Coq-Elpi 1.15 to 1.17.1 (except 1.17.0).

  • It provides the lra, nra, and psatz tactics for MathComp (contributed by Pierre Roux). For now, these tactics are considered experimental features and subject to change.
  • All the provided tactics now support Nat.of_num_uint of type Number.uint -> nat without triggering computation in nat.
Assets 2
Loading