From d8b37fe652d15d3a74b189c9d258c9ac189b0f4c Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Mon, 16 Sep 2019 17:51:06 +0200
Subject: [PATCH] fix README more

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

diff --git a/README.md b/README.md
index 896cf42..6a25fec 100644
--- a/README.md
+++ b/README.md
@@ -37,6 +37,8 @@ The directory structure is as follows:
   - Properties of the simulation with respect to the operational semantics are
   proven in `sim/body.v`, `sim/refl_pure_step.v`, `sim/refl_mem_step.v`,
   `sim/left_step.v`, `sim/right_step.v`, `sim/simple.v`.
+  - The fundamental property that the simulation is reflexive is proven in
+  `sim/refl.v`.
   - The main invariant needed for these properties is in `sim/invariant.v`.
 * `theories/opt`: Proofs of optimizations.
 
-- 
GitLab