Overview
========

This is a standalone version of the Ltac2 plugin. Ltac2 is an attempt at
providing the Coq users with a tactic language that is more robust and more
expressive than the venerable Ltac language.

Status
========

It is mostly a toy to experiment for now, and the implementation is quite
bug-ridden. Don't mistake this for a final product!

Installation
============

This should compile with Coq master, assuming the `COQBIN` variable is set
correctly. Standard procedures for `coq_makefile`-generated plugins apply.

Demo
====

Horrible test-files are provided in the `tests` folder. Not for kids.