v2.2.1

Fixed the build process from v2.2.0 (missing make files in htt and examples directories).

v2.2.0

Adapting to coq-fcsl-pcm 2.2.0 along with other dependencies (coq 9.0 and mathcomp 2.4.0).
Dropped support for coq 8.0 and mathcomp 2.3.0.

2.1.0

• A new minor release to support Hierarchy Builder 1.8 and coq-fcsl-pcm v2.1.0
• Added lemma for backward symbolic execution (bnd_vrf) in htt/model.v
• Added makefiles to build packages (suggested by Karl Palmskog).

2.0.1

• Reorganized subpackages to simplify client dependencies: coq-htt now depends on coq-htt-core.

2.0.0

• A new major release based on mathcomp2.
• Dropped coq8.15-8.17, support 8.19-8.20.
• STsep notation changed. Instead of {G}. STsep (p, q) now it's STsep {G} (p, q).
• The proof of Barcelogic congruence closure is restored (from POPL 2010 paper)

1.3.0

• removed examples from the opam release
• bumped minimal mathcomp to 1.17 and coq range to 8.15-8.17
• mathcomp-algebra is a new dependency (needed for interval.v)
• added examples/quicksort.v and refactored examples/bubblesort.v to use slice theory
• added small theory of slice surgery to interlude.v

1.2.0

• update to FCSL-PCM 1.7.0
• add a bubblesort example and corresponding dependency on fingroup
• add local options file with Program settings
• change namespace to lowercase htt
• move core files to /htt folder
• minor refactorings

1.1.0

• Allow for Coq 8.16 and Mathcomp 1.15
• Switch to FCSL-PCM 1.6
• Add specialized frame lemmas gU/stepU/tryU for passing an empty heap to a subroutine/recursive call
• Refactor gE/stepE/tryE frames lemmas to produce separate goals for value and exception cases - the latter is typically trivial, saving one case invocation
• Add GCD, binary (search) tree & cyclic buffer examples

1.0.0

The first public release of the HTT system