Template Coq

Template Coq

Build Status Gitter

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 this representation of terms, Template Coq includes:

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


The 8.8 branch documentation (coqdoc files) and pretty-printed HTML versions of the translations are available.



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:

Examples of plugins

Installation instructions

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 coq-8.8 branch.


To compile the library, you need:

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 Coq if 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 basic OCaml 4.04.1 compiler, and puts you in the right environment (check with ocamlc -v).

Once in the right switch, you can install Coq using:

# opam pin add coq 8.8.1 

Pinning coq prevents opam from trying to upgrade it afterwards, in this switch. If the command is successful you should have coq available (check with coqc -v).


Once in the right environment, Use:

Install with OPAM (for 8.6 version only)

Add the Coq repository:

opam repo add coq-released https://coq.inria.fr/opam/released

and run:

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

Check 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