Skip to content

Algebra Tactics 0.3.0
Compare
Choose a tag to compare
@pi8027 pi8027 released this 08 Feb 11:40
· 102 commits to master since this release
0.3.0
27d24b9
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.13 to 8.15, MathComp 1.12 to 1.14, Mczify 1.1 to 1.2, and Coq-Elpi 1.10.1 to 1.13. It fixes some performance issues, and provides experimental options to skip checking of some definitional equations that must hold regardless of whether the goal equation is valid or not, using the exact_no_check tactic:

Ltac ring_reflection ::= ring_reflection_no_check.
Ltac field_reflection ::= field_reflection_no_check.
Assets 2
Loading