diff --git a/README b/README
index 29e7ec3..72135e6 100644
--- a/README
+++ b/README
@@ -4,3 +4,9 @@ If a triple { P } s { Q } is valid in the model, then it is derivable
 using the rules in Hoare.v (see the inductive type `hoare_triple`).
 
 Requires std++: <https://gitlab.mpi-sws.org/iris/stdpp>.
+(Tested with git version f8719169e3ed75123d88c59d292ddd0972351ad3).
+
+
+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.