Skip to content

Template-Coq v2.1~beta2 for Coq 8.8

Pre-release
Pre-release
Compare
Choose a tag to compare
@mattam82 mattam82 released this 08 Aug 10:23
· 1600 commits to coq-8.8 since this release
v2.1-beta2
c81ffca
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.

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.

Assets 2