From 319e74a37f4eedc6896f9d8cf185a04816b1b998 Mon Sep 17 00:00:00 2001
From: Guillaume Claret <dev@clarus.me>
Date: Tue, 24 Mar 2015 18:32:33 +0100
Subject: [PATCH] README

---
 README.md | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 418ff72..c7de18f 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,20 @@
-# False
+# Falso
 A proof of false.
+
+This is an implementation in Coq of the [Falso](http://inutile.club/estatis/falso/) proof system.
+
+## Use
+Install with OPAM for Coq:
+
+    opam repo add coq-stable https://github.com/coq/repo-stable.git
+    opam install coq:falso
+
+In a tedious development:
+
+    Require Import Falso.All.
+
+    Lemma hard : forall (A : Prop), A.
+      destruct falso.
+    Qed.
+
+    Print Assumptions hard.