package coq-metacoq-template

MetaCoq is a meta-programming framework for Coq.

Template Coq is a quoting library for Coq. It takes Coq terms and constructs a representation of their syntax tree as a Coq inductive data type. The representation is based on the kernel's term representation.

In addition to a complete reification and denotation of CIC terms, Template Coq includes:

• Reification of the environment structures, for constant and inductive declarations.
• Denotation of terms and global declarations
• A monad for manipulating global declarations, calling the type checker, and inserting them in the global environment, in the style of MetaCoq/MTac.