Template Coq is a quoting library for Coq. It
Coq terms and constructs a representation of their syntax tree as
Coq inductive data type. The representation is based on the kernel’s
In addition to this representation of terms, Template Coq includes:
Reification of the environment structures, for constant and inductive declarations.
Denotation of terms and global declarations
Complete reification and denotation of CIC terms, including universes
A monad for manipulating global declarations, calling the type checker, and inserting them in the global environment, in the stype of MetaCoq/MTac.
A partial type-checker for the Calculus of Inductive Constructions, runable as a plugin.
Example plugins built on top of this.
The coq-8.8 branch is the active development branch. If possible, it’s strongly recommended to use this branch.
The branch coq-8.6 is stable, but only contains the first two features in the above list. The coq-8.7 is stable and contains all features, but may not receive new ones.
The branch master tracks the current Coq
The 8.8 branch documentation (coqdoc files) and pretty-printed HTML versions of the translations are available.
The system was presented at Coq’PL 2018
“Towards Certified Meta-Programming with Typed Template-Coq” A. Anand, S. Boulier, C. Cohen, M. Sozeau and N. Tabareau. ITP’18
Template-Coq was originally developed by Gregory Malecha, and is now developed by Abhishek Anand, Simon Boulier and Matthieu Sozeau.
Contributors include Yannick Forster, Cyril Cohen and Nicolas Tabareau.
Copyright (c) 2014-2018 Gregory Malecha\
Copyright (c) 2015-2018 Abhishek Anand, Matthieu Sozeau\
Copyright (c) 2017-2018 Simon Boulier, Nicolas Tabareau, Cyril Cohen
This software is distributed under the terms of the MIT license. See LICENSE for details.
The current development branch is coq-8.8, which includes:
The full syntax of CIC: Ast
The typing judgment of CIC: Typing
A partial type-checker implementation: Checker
TemplateMonaddatatype and the
Run TemplateProgramcommand to run template programs: TemplateMonad
Examples of plugins
- a plugin to add a constructor in test-suite/add_constructor.v
- a parametricity plugin in translations/tsl_param.v
- a plugin to negate funext in translations/fun.v
Install the 8.8 version from scratch
To get the source code:
# git clone https://github.com/Template-Coq/template-coq.git # git checkout -b coq-8.8 origin/coq-8.8 # git status
Check that you are indeed on the
To compile the library, you need:
Coq 8.8.1(8.8.0 might work as well) and
4.04.1, beware that
OCaml 4.06.0can produce linking errors on some platforms).
Requirements through opam
The easiest way to get both is through opam:
You might want to create a “switch” (an environment of
opam packages) for
you don’t have one yet:
# opam switch -A 4.04.1 coq.8.8.1 # eval `opam config env`
This creates the
coq.8.8.1 switch which initially contains only the
4.04.1 compiler, and puts you in the right environment
Once in the right switch, you can install
# opam pin add coq 8.8.1
coq prevents opam from trying to upgrade it afterwards, in
this switch. If the command is successful you should have
available (check with
Once in the right environment, Use:
maketo compile the template-coq plugin (and the checker in
make translationsto compile the translation plugins (in
make test-suiteto compile the test suite
make installto install the plugin in
coq’s user-contrib local library. Then the
Templatenamespace can be used for
Require Importstatements, e.g.
From Template Require Import All..
Install with OPAM (for 8.6 version only)
Add the Coq repository:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-template-coq
To get beta versions of Coq, you might want to activate the repository:
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
How to Use
test-suite/demo.v for examples.
Unless you installed the library, you must add the theories directory to your Coq load path with the prefix Template. This can be done on the command line by adding:
coqc ... -R <path-to-theories> -as Template ...
or inside a running Coq session with:
Add LoadPath "<path-to-theories>" as Template.
Because paths are often not portable the later is not recommended.
If you use Emacs and Proof General, you can set up a .dir-locals.el with the following code:
((coq-mode . ((coq-load-path . ( (nonrec "<absolute-path-to-theories>" "Template") )))))
As long as you don’t check this file into a repository things should work out well.
Please report any bugs (or feature requests) on the github issue tracker