diff --git a/INSTALL.md b/INSTALL.md
index cb7cb19..b905d4a 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -1,6 +1,12 @@
 
-Once Coq is properly setup (see REQUIREMENTS.md), you can simply issue `make` in the root folder and browse the proof with your favourite Coq IDE.
+Once Coq is properly setup (see REQUIREMENTS.md), you can simply issue `make` in the root folder and browse the proof with your favourite Coq IDE:
+```
+make
+```
 
 Alternatively, instructions for using a docker container are provided in DOCKER.md.
 
-For easiness, the html documentation built using `coqdoc` is included in the artefact. It can be built again invoking `make coqdoc`.
+For easiness, the html documentation built using `coqdoc` is included in the artefact. It can be built again invoking
+```
+make coqdoc
+```
diff --git a/REQUIREMENTS.md b/REQUIREMENTS.md
index 193035b..25be5b8 100644
--- a/REQUIREMENTS.md
+++ b/REQUIREMENTS.md
@@ -1,8 +1,10 @@
 
 # Software Requirements
 
-The project builds with Coq version `8.16.1`. It depends on the opam package `coq-smpl` and `coq-equations` (version 1.3 at least). After setting up [opam](https://opam.ocaml.org/doc/Usage.html), the proper environment is installed with
+The project builds with [Coq](https://coq.inria.fr/) version `8.16.1`. It depends on the opam package `coq-smpl` and `coq-equations` (version 1.3 at least). After installing [opam](https://opam.ocaml.org/) with your favorite package manager, the proper environment is setup and installed with
 ```
+opam init
+eval $(opam env)
 opam install coq.8.16.1 coq-equations.1.3+8.16 coq-smpl.8.16
 ```