blob: d49dd8807694f962067d4204d7ab502d9eeeed97 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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.
|
