Releases: coq-community/huffman
Releases · coq-community/huffman
Huffman 8.16.0 maintenance release
Huffman 8.15.0 maintenance release
Release with Coq 8.15 and 8.16 compatibility.
Huffman 8.14.0 maintenance release
Maintenance release with Coq 8.14 compatibility.
Huffman 8.13.0 maintenance release
Maintenance release with Coq 8.13 compatibility, featuring the following changes:
- adjust hint locality to avoid global hints
- use permutation predicate from the standard library
Huffman 8.12.0 maintenance release
Maintenance release with Coq 8.12 compatibility, featuring the following changes:
- update metadata and documentation
- optional support for building and extracting code with Dune
Huffman 8.11.0 maintenance release
Maintenance release with Coq 8.11 compatibility, featuring the following changes:
- replace tactic-built functions with Gallina using
Program
- use stdlib in place of some utility functions and lemmas
- update metadata and documentation
Huffman 8.10.0 maintenance release
Maintenance release with Coq 8.10 and 8.11+beta1 compatibility, featuring the following changes:
- update documentation, add link to technical report
- Coq-only default build
- build parameter fixes
Huffman 8.9.0 maintenance release
Maintenance release after move to Coq-community, with Coq 8.9 compatibility, featuring the following changes:
- consistently parameterize lists on element types in
Type
rather than inSet
for generality - add
Proof using
annotations for better parallel proving - modernize the build scripts to use
coq_makefile
features