Quieting the build

[JasonGross]

The build is quite noisy, filled with messages like

File "./theories/Categories/Functor/Composition/Laws.v", line 43, characters 0-55:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]

We should either fix the hints or suppress the warning.

[Alizter]

This is when it is built with master no? On 8.13.1 I see no warnings.

[Alizter]

These have been fixed and other warnings in the meantime have been dealt with or appropriately silenced.