Things missing in the changelog
- The latest
Infinite
changes.
- The multiset name changes.
- Dropping support for Coq 8.6; supporting Coq 8.9.
- Repo moved to a new location.
- There's generated coqdoc documentation (but for master only, not for releases...)
- A definition of basic telescopes + some theory about them.
A simple type class based canceler for natural numbers.
- There are also quite a few new lemmas etc, aren't there? For example
- Make
default
an abbreviation for from_option id
(instead of just swapping the argument order of from_option
)
- More results about
Qp
fractions, and avoid overwriting their Coq stdlib notation.
- Notation
=@{A}
, ≡@{A}
, ∈@{A}
, ##@{A}
, ⊆@{A}
, ⊂@{A}
, ⊑@{A}
, ≡ₚ@{A}
for being explicit about the type.
- Define a
size
for finite maps and prove some properties.
Edited by Ralf Jung