Add `Declare Scope` where appropriate (#440)

And re-enable the `undeclared-scope` warning.

`Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.

3 files changed, 5 insertions, 0 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 08e0a4f4..4de215b8 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -167,6 +167,8 @@ Definition check_succ (s: node) (b: LTL.bblock) : bool :=
   | _ => false
   end.
 
+Declare Scope option_monad_scope.
+
 Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end)
          (at level 200, X ident, A at level 100, B at level 200)
          : option_monad_scope.
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index f6f6e34d..97a666bd 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -54,6 +54,7 @@ with condexpr : Type :=
   | CEcondition : condexpr -> condexpr -> condexpr -> condexpr
   | CElet: expr -> condexpr -> condexpr.
 
+Declare Scope cminorsel_scope.
 Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope.
 
 (** Conditional expressions [condexpr] are expressions that are evaluated
diff --git a/backend/Registers.v b/backend/Registers.v
index 622cddfe..7f7ecb60 100644
--- a/backend/Registers.v
+++ b/backend/Registers.v
@@ -61,6 +61,8 @@ Definition regmap_setres
   | _ => rs
   end.
 
+Declare Scope rtl.
+
 Notation "a # b" := (Regmap.get b a) (at level 1) : rtl.
 Notation "a ## b" := (List.map (fun r => Regmap.get r a) b) (at level 1) : rtl.
 Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level) : rtl.