A quoting and unquoting library for Coq in 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. - A partial type-checker for the Calculus of Inductive Constructions, runable as a plugin. - Example plugins built on top of this.
opam install coq-template-coq.2.0~beta