Fix undeclared scope warnings

[anton-trunov]

Coq 8.10+alpha emits warnings like this one:

File "./theories/rels.v", line 38, characters 0-33:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope rel_scope.". [undeclared-scope,deprecated]

[anton-trunov]

@Zimmi48, @palmskog Is there a way to fix these warnings without branching on Coq versions? AFAIK, Coq 8.8 does not support Declare Scope.

[Zimmi48]

No, I don't think there is a way, except to locally disable these warnings: Set Warnings "-undeclared-scope".

[palmskog]

I would definitely vote for not using the Declare Scope syntax for now, but leaving this issue open. It worries me a bit that Declare Scope seems not to be currently supported in Coq 8.9beta1.

Is it the plan to deprecate the old syntax and introduce the new syntax in the same major Coq version @Zimmi48? I think a reasonable policy for this project would be to only use the new syntax once one new stable version is released after the version introducing the syntax.

[Zimmi48]

Indeed.

[anton-trunov]

I think a reasonable policy for this project would be to only use the new syntax once one new stable version is released after the version introducing the syntax.

Does it mean we should retag this issue as needs Coq 8.11? I understand this quote as "we should support at least two latest stable releases" and Declare Scope only landed in in Coq 8.10.

[Zimmi48]

@anton-trunov My understanding of the "needs Coq 8.10" label is: the lowest supported version needs to be Coq 8.10 before we can close this issue. This is also the meaning behind "needs: newer OCaml" in the Coq repository.