diff --git a/doc/guidelines.md b/doc/guidelines.md
index 04618c3590a65209ed48f0647b3cbc3b14935440..6572c1bcf49ed09e8783854419550fccf5564d6a 100644
--- a/doc/guidelines.md
+++ b/doc/guidelines.md
@@ -29,6 +29,7 @@ This project targets Coq *non*-experts. Accordingly, great emphasis is placed on
     Hypothesis H_sporadic_tasks:
       sporadic_task_model task_period arr_seq job_task.
 ```
+- When commenting, be careful not to leave any mispelled word: Prosa's CI system comprises a spell-checker that will signal any error. When comments have to contain variable names or mathematical notation, use square brackets (e.g. `[job_cost j]`). You can nest square brackets _only if they are balanced_: `[[t1,t2)]` will not work. In this case, use `<<[t1,t2)>>`.
 - Document the sources of lemmas and theorems in the comments. For example, say something like "Theorem XXX in (Foo & Bar, 2007)", and document at the beginning of the file what "(Foo & Bar, 2007)" refers to.