Skip to content


Repository files navigation


Docker CI Contributing Code of Conduct Zulip DOI

Autosubst is a library for the Coq proof assistant which provides automation for formalizing syntactic theories with variable binders. Given an inductive definition of syntactic objects in de Bruijn representation augmented with binding annotations, Autosubst synthesizes the parallel substitution operation and automatically proves the basic lemmas about substitutions.


Building and installation instructions

The easiest way to install the latest released version of Autosubst is via OPAM:

opam repo add coq-released
opam install coq-autosubst

To instead build and install manually, do:

git clone
cd autosubst
make   # or make -j <number-of-cores-on-your-machine> 
make install

To build the examples that do not need ssreflect, type

make examples-plain

The examples that depend on ssreflect are built with

make examples-ssr

To build the documentation (including all examples), type

make doc

You can use the file doc/toc.html to browse the documentation.

Bug Reports

Please submit bugs reports on