From cf934bceae42bb98913a56f75826443ffc19c213 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 9 Jul 2021 11:47:21 +0200
Subject: [PATCH] tweak readme some more

---
 README.md | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index eb39c56d..6012af74 100644
--- a/README.md
+++ b/README.md
@@ -8,8 +8,9 @@ This project is known to build with [Coq 8.13.2](https://coq.inria.fr/).
 It depends on recent development versions of [std++](https://gitlab.mpi-sws.org/iris/stdpp) and [Iris](https://gitlab.mpi-sws.org/iris/iris), as well as [coq-equations](https://github.com/mattam82/Coq-Equations).
 
 We recommend using [opam](https://opam.ocaml.org/) (version >= 2.0, tested on 2.0.8) for the installation.
+
 ### With opam
-We have bundled archived versions of `stdpp` and `iris` known to be working with this project.
+We have bundled the versions of `stdpp` and `iris` known to be working with this project.
 Please execute the following instructions in the folder containing this README (replacing `N` with the number of jobs you'd like to use for compilation).
 ```
 opam switch create simuliris 4.11.1
@@ -77,6 +78,7 @@ The project follows the following structure below the `theories` folder:
 
 ## Theorems, definitions, and examples referenced in the paper
 We list the relevant theorems and definitions mentioned in the paper by section.
+
 ### Section 2
 | Paper | Coq file | Coq name |
 | ------ | ------ | ------ |
@@ -95,7 +97,6 @@ We list the relevant theorems and definitions mentioned in the paper by section.
 | Rule `while-coind` (2.4) | `theories/simulang/simple_inv/examples/derived.v` | `sim_while_simple` |
 | Rule `while-paco` (2.4) | `theories/simulang/simple_inv/examples/derived.v` | `sim_while` |
 
-
 ### Section 3
 | Paper | Coq file | Coq name |
 | ------ | ------ | ------ |
@@ -124,7 +125,6 @@ They are instantiated for the fundamental theorems.
 | Theorem 4.2 (for SimuLang, non-atomic logic) | `theories/simulang/na_inv/refl.v` | `log_rel_ctx` |
 | Theorem 4.3 (for SimuLang, non-atomic logic) | `theories/simulang/na_inv/adequacy.v` | `log_rel_adequacy` |
 
-
 ### Section 5
 | Paper | Coq file | Coq name |
 | ------ | ------ | ------ |
@@ -155,7 +155,6 @@ They are instantiated for the fundamental theorems.
 | Loop example (Fig 12b) | `theories/stacked_borrows/examples/coinductive.v` | `sim_loop_ctx` |
 | Moving read example (Fig 12a) | `theories/stacked_borrows/examples/opt1.v` | `sim_opt1'` |
 
-
 The optimizations ported and extended to concurrency from the original Stacked Borrows paper can be found in the following files:
 * `theories/stacked_borrows/examples/opt1.v`
 * `theories/stacked_borrows/examples/opt1_down.v`
@@ -167,4 +166,3 @@ The optimizations ported and extended to concurrency from the original Stacked B
 ### Section 8
 As mentioned in the related work section, we have verified the reorderings and eliminations by [Ševčík, 2011]. They can be found in file `theories/simulang/na_inv/examples/program_transformations_in_weak_memory_models.v`.
 For further information on this, we refer to Section 5 of the technical appendix.
-
-- 
GitLab