Commit 0440ebb4 authored by David Swasey's avatar David Swasey

erasure -> world satisfaction

parent 14ff5436
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment