From 517748db8a566b8c112f8ea7608c0faaf3e4b87b Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 14 Jun 2019 19:52:10 +0200
Subject: [PATCH] add a fair warning to README.md

---
 README.md | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 344b193..75e027e 100644
--- a/README.md
+++ b/README.md
@@ -2,4 +2,9 @@ Formalisation of ["Noninterference, Transitivity, and Channel-Control Security P
 
 Requires [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp).
 
-The proofs are in `Rushby.v`.
+The proofs are in `Rushby.v` and one instantiation is in `ArrayMachine.v`.
+
+
+BEWARE!!! I wrote this formalization when I started my PhD, and I
+didn't know much about (idiomatic) Coq back then. As a result, the
+code is quite shitty.