diff options
| -rw-r--r-- | README.md | 23 |
1 files changed, 23 insertions, 0 deletions
@@ -0,0 +1,23 @@ +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 langue. + +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 8.7, assuming the `COQLIB` 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. |