Add `Declare Scope` where appropriate

[xavierleroy]

Declare Scope makes it possible to declare a new notation scope before adding notations to it. This construct has been available since Coq 8.12, and is recommended, to the point that a warning is triggered (by default) if a notation is added to an undeclared scope.

Now that 8.12 is the lowest supported Coq version, we can use Declare Scope and stop silencing the undeclared-scope warning.