Skip to content

1.8.0
Compare
Choose a tag to compare
@aleksnanevski aleksnanevski released this 10 May 12:39
· 18 commits to master since this release
v1.8.0
b2aa833
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.
  • allow Coq 8.17, drop 8.14
  • allow Mathcomp 1.16, drop 1.13-14
  • add mathcomp-algebra dependency
  • add Prop-level theory for All and Has
  • rename AllPn->allPnIn, HasPn->hasPnIn
  • add trans_eq, if_triv, theory for foldl/r and onth in prelude, rename prefixP -> prefixE
  • expand seq theory in seqext, including "big cat" lemmas
  • refactor slice theory, split interval theory on unique sequences into useqord, uslice and uconsec
Assets 2
Loading