From cac89cbf64e789094f58ec3827e4249dcec7be64 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Sat, 14 Jan 2017 11:39:10 +0100
Subject: [PATCH] Update README.md

---
 README.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index cd02ea35..fe6d11d9 100644
--- a/README.md
+++ b/README.md
@@ -26,9 +26,11 @@ and then `make` in [coq/ra](coq/ra).
 
 ### Structure
 
-* The language is in `lang.v`. The operational semantics is in `machine.v`.
+* The operational semantics is in `machine.v`. The language is in `lang.v`.
 * The base logic is in the `base` folder. The model is in `base/ghosts.v`.
+  Each base rule is proven in a separate file.
 * iRSL's main rules are in `rsl_instances.v`. The model is in `rsl.v`.
 * Non-atomic rules are in `na.v`.
 * iGPS's rules are in the `gps` folder. The model is in `gps/shared.v`
-* Examples are in the `examples` folder.
\ No newline at end of file
+* Examples are in the `examples` folder.
+* `tests/message_passing.v` contains a closed proof of MP without Iris statements.
\ No newline at end of file
-- 
GitLab