From f00f5b1b74449ccd475887f11b16fe4798f8bd22 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Mon, 11 Sep 2017 10:47:09 +0200
Subject: [PATCH] Added recommended software.

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

diff --git a/README.md b/README.md
index cb731b7..9160de3 100644
--- a/README.md
+++ b/README.md
@@ -81,3 +81,15 @@ We also show the limits of dependently-typed functional programming.
 * Total functional programming.
 * Generic functional programming.
 * Open problems in dependent functional programming.
+
+## Recommended software
+
+OCaml 4.0x and Coq **8.5**.
+
+Once you have installed [opam](https://opam.ocaml.org/doc/Install.html), use the following commands:
+```bash
+opam init --comp=4.05 # for instance
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam update
+opam install -j4 -v coq.8.5.3
+```