diff --git a/README.md b/README.md
index cf4e1db4c592edda9e250e29fff9c4f853647347..1cc3d966ee05a10c7c8422fd71425ba081207720 100644
--- a/README.md
+++ b/README.md
@@ -12,14 +12,20 @@ The master branch is known to compile with:
 
 ## Build
 
-The easiest way to build the development is to use OPAM.
-Go to [coq/ra](coq/ra) and then `make build-dep`.
-All the dependencies will be built and installed by OPAM before
-the actual compilation of the development.
+The recommended way to build the development is using OPAM. To avoid conflicts
+with existing packages, we recommend to create a new opam switch:
 
-Manually, one can build and install Iris
-(currently [Iris@01d12014][iris]),
-and then `make` in [coq/ra](coq/ra).
+`opam switch ra-gps --alias-of=4.02.3`
+
+It should work for any compiler version upwards of 4.01.0. After compiling
+OCaml, the new switch needs to be activated in your current shell. opam will
+print the necessary instructions.
+
+To find all the dependencies of ra-gps, opam needs to know about the Coq opam archive. This can be achieved by executing
+`opam repo add coq-released https://coq.inria.fr/opam/released`
+
+Now, go to [coq/ra](coq/ra) and execute `make build-dep` to install all
+dependencies of ra-gps. Finally, execute "make" to build the development.
 
 ## Structure
 
@@ -28,6 +34,7 @@ The Coq development is in folder [coq/ra/](coq/ra).
 * The operational semantics is in [machine.v](coq/ra/machine.v). The language is in [lang.v](coq/ra/lang.v).
 * The base logic is in the [base/](coq/ra/base) folder.
   Each base rule is proven in a separate file.
+<<<<<<< Updated upstream
 * iRSL's main rules are in [rsl_instances.v](coq/ra/rsl_instances.v). The model is in [rsl.v](coq/ra/rsl.v).
 * Non-atomic rules are in [na.v](coq/ra/na.v).
 * iGPS's rules are in the [gps/](coq/ra/gps) folder. The model is in [gps/shared.v](coq/ra/gps/shared.v)
@@ -55,3 +62,10 @@ The Coq development is in folder [coq/ra/](coq/ra).
 
 
 [iris]: https://gitlab.mpi-sws.org/FP/iris-coq/commit/01d12014855abe6adaea20bbb35b1e9beadff14e
+=======
+* iRSL's main rules are in `rsl_instances.v`. The model is in `rsl.v`.
+* Non-atomic rules are in `na.v`.
+* iGPS's rules are in the `gps` folder. The model is in `gps/shared.v`
+* Examples are in the `examples` folder.
+* `tests/message_passing.v` contains a closed proof of MP without Iris statements.
+>>>>>>> Stashed changes