From 2c9233d40d75492fa7f06c09c2bf4f7b16fd1280 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Jul 2017 18:49:10 +0200
Subject: Filling the README.

---
 README.md | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

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.
-- 
cgit v1.2.3