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