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.
It is mostly a toy to experiment for now, and the implementation is quite bug-ridden. Don't mistake this for a final product!
This should compile with Coq master, assuming the COQBIN variable is set
correctly. Standard procedures for coq_makefile-generated plugins apply.
Horrible test-files are provided in the tests folder. Not for kids.