diff --git a/README.md b/README.md
index 26f984239..621288f26 100644
--- a/README.md
+++ b/README.md
@@ -36,6 +36,29 @@ variables, i.e. reuse λProlog's meta variables to implement Coq's ones.
 
 ## How to install coq-elpi
 
+### Released version
+
+Version 0.1.x can be installed via OPAM. It works on the v8.9 branch
+of Coq.
+
+```shell
+opam repo add coq-dev http://coq.inria.fr/opam/core-dev
+opam repo add extra-dev http://coq.inria.fr/opam/extra-dev
+opam install coq-elpi
+```
+
+The part of the software that is released is the derive command, documented
+by [Deriving proved equality tests in Coq-elpi](https://hal.inria.fr/hal-01897468).
+
+```coq
+From elpi Require Import derive.
+Elpi derive nat.
+```
+
+The is also an [online demo](https://lpcic.github.io/coq-elpi-www/tutorial-demo_derive.html) that requires no installation.
+
+### Development version
+
 The simplest way is to use [OPAM](http://opam.ocaml.org/) and type
 ```
 opam pin add coq-elpi https://github.com/LPCIC/coq-elpi.git
@@ -50,7 +73,6 @@ Thanks to [jscoq](https://github.com/ejgallego/jscoq) you can play the following
 - [tutorial on the Elpi λProlog dialect](https://lpcic.github.io/coq-elpi-www/tutorial-elpi_lang.html) 
 - [tutorial on coq-elpi](https://lpcic.github.io/coq-elpi-www/tutorial-coq_elpi.html) 
 - [demo at CoqPL2018](https://lpcic.github.io/coq-elpi-www/tutorial-demo_CoqPL2018.html)
-- [demo_derive](https://lpcic.github.io/coq-elpi-www/tutorial-demo_derive.html)
 
 
 ### Syntax highlight in CoqIDE