diff --git a/README.md b/README.md
index f10889e186c1d4a20d4a58032d47da84a353293c..c58272311829d8665ea4168b3fb1036b344309b5 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # Simuliris Coq development
 
-This repository contains the Coq development of Simuliris (paper presented at POPL22: https://iris-project.org/pdfs/2022-popl-simuliris.pdf).
+This repository contains the Coq development of Simuliris, additionally including the Tree Borrows Optimization Program Logic, and also some Tree Borrows optimizations not proven via Simuliris.
 
 ## Prerequisites
 
@@ -21,9 +21,10 @@ installing the dependencies.  This requires the following two repositories:
 Once you got opam set up, run `make build-dep` to install the right versions
 of the dependencies.
 
+Then run `make` to build everything.
+
 ## Structure
-We include our fork of simuliris in its entirety.
-In particular, that includes the data-race reasoning examples from the simuliris paper, as well as the Stacked Borrows development, which are not the focus of our paper.
+Our fork of simuliris in particular includes the upstream version, which proves things about Simuliris, or about data races (in weak memory model), which is part of this archive file but not relevant for the paper.
 The Tree Borrows development lives in `theories/tree_borrows` and has its own `README.md`, please consult that.
 
 
@@ -45,4 +46,4 @@ The project follows the following structure below the `theories` folder:
 
 ## More information
 
-See the `README.md` in `theories/tree_borrows`
\ No newline at end of file
+See the `README.md` in `theories/tree_borrows`
diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md
index 2f0ac37f0d841f2fa93df386232ceaa8d3dcce94..b9460154f79bc25661e0a85508a3303e79548059 100644
--- a/theories/tree_borrows/README.md
+++ b/theories/tree_borrows/README.md
@@ -43,7 +43,7 @@ This example corresponds to the one in `examples/protected/mutable_reorder_write
 This Coq example corresponds very closely to the one in the paper.
 The only difference is that `f` and `g` have an extra argument in Coq, which corresponds to the implicit environment that closures have in Rust.
 
-### Paragraph 3: Reordering Reads (Example 18)
+### Paragraph 4: Reordering Reads (Example 18)
 
 This is proven in `read_read_reorder`, particularly in `refinement.v`.
 These proofs do not use the `simuliris` library, but instead they do a much simpler equivalence proof directly against the operational semantics.
@@ -62,6 +62,6 @@ We have not shown Example 14, but two examples similar to it:
   But note that this does not insert a read if there is none. Also, the tag is not protected.
 * `examples/protected/shared_insert_read.v` demonstrates that reads can be inserted on protected tags.
 
-For the artifact submission, we will create a new example that corresponds to Example 14 more closely.
+For the artifact evaluation submission, we will create a new example that corresponds to Example 14 more closely.