This reverts commit 20b4ae55, which does not seem to work with Coq 8.5pl2 (I accidentally tested with 8.5pl1).