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.