From 0440ebb4e6ef656d7670b48112a726463e807966 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Wed, 4 Feb 2015 17:41:07 +0100
Subject: [PATCH] erasure -> world satisfaction

---
 README.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.txt b/README.txt
index 2500c4d3d..7b737cec8 100644
--- a/README.txt
+++ b/README.txt
@@ -56,7 +56,7 @@ CONTENTS
   * world_prop.v uses the ModuRes Coq library to construct the domain
     for Iris propositions
   
-  * iris_core.v defines erasure and the simpler assertions
+  * iris_core.v defines world satisfaction and the simpler assertions
   
   * iris_vs.v defines view shifts and proves their rules
   
-- 
GitLab