Addressing Coq warnings

It is very recommended that package maintainers address warnings emitted by Coq as early as possible (in particular deprecation warnings) as this will generally reduce the maintenance burden later on. We generally recommend a warning-free build. This can be ensured by passing the -w +default flag to coqc which turns all default warnings into errors. It can be followed by other flags of the form -w -foo, for instance -w -notation-overriden to silence warnings that are voluntarily not fixed. This is particularly useful to silence deprecation warnings when the only way of fixing them would break compatibility with older Coq versions (in this case, we recommend opening an issue to remember to stop silencing these warnings when support for the older Coq version is discontinued, example: coq-community/lemma-overloading#28).

For Coq packages built with coq_makefile we recommend using a _CoqProject file of the following form:

-Q theories MyPackageNamespace

-arg -w -arg +default
-arg -w -arg -warning-to-silence-1
-arg -w -arg -warning-to-silence-2

This way of passing the -w flags is understood by coq_makefile, CoqIDE and recent versions of Proof-General.