diff --git a/README.md b/README.md
index 0233f9e..7464344 100644
--- a/README.md
+++ b/README.md
@@ -21,7 +21,7 @@ Now proceed to install the dependencies:
 ```
 cd semantics-2023
 
-# We create a new "switch" to install the dependencies in. Switches are independent 
+# We create a new "switch" to install the dependencies in. Switches are independent
 # installation prefixes with their own set of installed packages.
 opam switch create semantics ocaml-base-compiler.4.14.1
 # We tell opam to automatically enable the switch `semantics` in this directory
@@ -49,6 +49,8 @@ make -j4
 ```
 **IMPORTANT:** You will have to compile to interactively do proofs. You will have to recompile if the dependencies of the file your editing change.
 
+By default, the exercise proofs won't be compiled by the above command.
+You can still work on them interactively, but if you want `make` to check them, you will need to append their path to the `_CoqProject` file.
 
 ## Editing the Coq code
 To edit the Coq code and complete the exercises, you will need an editor. We recommend you use [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html) or [VsCoq](https://github.com/coq-community/vscoq) ([VSCode](https://code.visualstudio.com/)).