From 639d7951fc0e9a4ba4cc4c9f15480ef58ee0adad Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Fri, 20 Oct 2017 12:38:59 +0200
Subject: [PATCH] Link to Coq mini-demo.

---
 README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 7e35712..f04249f 100644
--- a/README.md
+++ b/README.md
@@ -92,7 +92,8 @@ We also show the limits of dependently-typed functional programming.
   * Transforming a graph traversal
     ([solution](ocaml/Graph.ml)).
 * (20/10/2017) Equational reasoning and program optimizations
-  ([slides 05](slides/fpottier-05.pdf)).
+  ([slides 05](slides/fpottier-05.pdf))
+  ([Coq mini-demo](coq/DemoEqReasoning.v)).
 
 ### Metatheory of Typed Programming Languages