I am pleased to announce the release of Bindlib 5.0.1, which is a library for handling structures with bound (and free) variables (typical applications include the development of languages and proof systems). It has already been available on Opam for several weeks, and the source code of the latest version can be found in the development repository.
This new version provides a simpler, more concise interface. It is extensively documented, and includes a small tutorial. An introductory paper has also been recently presented at the LFMTP 2018 workshop.
The implementation is very efficient (in terms of substitution), and it handles renaming to avoid capture.
Feel free to give feedback!