Mention how to compile exercises with make

README.md

@@ -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/)).