From a5594a3a35e1c09286cab78d0047bf3589f7c9cd Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Mon, 6 Oct 2014 17:09:12 +0200
Subject: [PATCH] Coq README update

---
 README.txt | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/README.txt b/README.txt
index 441e2baad..834800b0a 100644
--- a/README.txt
+++ b/README.txt
@@ -22,7 +22,7 @@ CONTENTS
   * lang.v defines the threadpool reduction and derives some lemmas from core_lang.v
   * masks.v introduces some lemmas about masks
   * world_prop.v uses the aforementioned Coq library to construct the domain for Iris propositions
-  * iris.v is the main file and contains the actual logic and the proof of the rules for view shifts and Hoare tiples
+  * iris.v is the main file and contains the actual logic and the proof of the rules for view shifts and Hoare triples
 
   It uses a Coq library in lib/ by Sieczkowski et al. to solve the recursive domain equation (see the paper for a reference).
 
@@ -59,12 +59,15 @@ OVERVIEW OF LEMMAS
   VSClose      vsClose
   VSTrans      vsTrans
   VSImp        vsEnt
-  GhostUpd     vsGhostUpd
+  VSFrame      vsFrame
+  FpUpd        vsGhostUpd
 
   Ret          htRet
   Bind         htBind
   Frame        htFrame
+  AFrame       htAFrame
   Csq          htCons
   ACSQ         htACons
+  Fork         htFork
 
   The main adequacy result is expressed by Theorem soundness_obs.
-- 
GitLab