<!-- Thank you for your contribution.
     Make sure you read the contributing guide and fill this template. -->


<!-- Keep what applies -->
**Kind:** documentation / bug fix / feature / performance / infrastructure.


<!-- If this is a bug fix, make sure the bug was reported beforehand. -->
Fixes / closes #????


<!-- If there is a user-visible change in coqc/coqtop/coqchk/coq_makefile behavior and testing is not prohibitively expensive: -->
<!-- (Otherwise, remove this line.) -->
- [ ] Added / updated test-suite
<!-- If this is a feature pull request / breaks compatibility: -->
<!-- (Otherwise, remove these lines.) -->
- [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
- [ ] Entry added in CHANGES.md.