Either because the code change that would silence the warning is not
desirable, or because it would break compatibility with earlier versions
of Coq.

Explain the silenced warnings as comments in the Makefile.