diff options
Diffstat (limited to 'vendor/Ltac2/README.md')
| -rw-r--r-- | vendor/Ltac2/README.md | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/vendor/Ltac2/README.md b/vendor/Ltac2/README.md new file mode 100644 index 0000000000..d49dd88076 --- /dev/null +++ b/vendor/Ltac2/README.md @@ -0,0 +1,25 @@ +[](https://travis-ci.org/ppedrot/ltac2) + +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. |