github MetaCoq/metacoq v2.1-beta
Template-Coq v2.1-beta for Coq 8.8

latest releases: v1.3.2-8.20, v1.3.2-8.19, v1.3.1-8.19...
pre-release6 years ago

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.
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.

Don't miss a new metacoq release

NewReleases is sending notifications on new releases.