Filling the README.

1 files changed, 23 insertions, 0 deletions

diff --git a/README.md b/README.md
index e69de29bb2..a5aa40eeb6 100644
--- a/README.md
+++ b/README.md
@@ -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.