Ensure that no unwanted TODOs or FIXMEs remain before merging

[maximedenes]

It would be a nice feature. Not sure if it should be the job of coqbot or a linter.

[Alizter]

Ideally part of the linter, but is it really what we want? Sometimes there are good reasons to leave TODOs.

[Zimmi48]

@jfehrle has a strategy of distinguishing todo PR (needs to be resolved before merging) and todo (for latter consideration). I've always been reluctant of adding TODOs in the code myself, but they can make sense when the point raised might be especially relevant for the next person looking at the code. It seems like lots of people have considering automatically creating issues from TODOs in code (https://www.google.com/search?client=firefox-b-d&q=todo+in+code+and+issues) and there is more generally quite some literature on TODO code comments (https://scholar.google.fr/scholar?hl=en&as_sdt=0%2C5&q=todo+code+comments&btnG=). Some reading for later (I don't have time for this right now, unfortunately 😉).

[maximedenes]

Let's not over-engineer things. The feature request is a warning. A reviewer or the PR author can then take the right decision.