blob: 4d6879d8afafa6b6a71c5f74ff39f3b4264d87ad (
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 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.
|
