diff --git a/README.txt b/README.txt
index 2500c4d3d6cea479a02329ffd7650f3d45bf88a2..7b737cec8028f2cf6c070ea22b6f05f647b11176 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