Skip to content

Template-Coq v2.1~beta3 for Coq 8.8

Pre-release
Pre-release
Compare
Choose a tag to compare
@mattam82 mattam82 released this 14 Aug 11:27
· 1581 commits to coq-8.8 since this release

This release reflects the current status of the Coq 8.8 branch of Template-Coq. It is not feature-complete but stability is expected for:

  • The Coq term AST, which reflects all the kernel Coq terms
  • The interfaces of the universe graph.
  • The Coq entries and declaration Asts, which reflect the structures to get declarations in and out of the kernel.
  • The interface of the checker/type-inference algorithm.
  • The template monad features (currently runnable in Coq only)

Work is in progress on:

  • The formalization of the typing derivations, in particular the missing pieces on (co)-fixpoints and inductives.
  • The correctness proofs of the typechecker.
  • The formalization of the extraction algorithm, stripping proof terms from Coq terms.

This release significantly departs from and is incompatible with series 1 by Gregory Malecha (see https://github.com/gmalecha/template-coq/releases) and the previous 8.6 and 8.7 versions.