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.

19 files changed, 31 insertions, 7 deletions

diff --git a/Makefile b/Makefile
index b3b7a124..48648a0a 100644
--- a/Makefile
+++ b/Makefile
@@ -44,9 +44,6 @@ endif
 
 # Notes on silenced Coq warnings:
 #
-# undeclared-scope:
-#    warning introduced in 8.12
-#    suggested change (use `Declare Scope`) supported since 8.12
 # unused-pattern-matching-variable:
 #    warning introduced in 8.13
 #    the code rewrite that avoids the warning is not desirable
@@ -58,7 +55,6 @@ endif
 #    triggered by Menhir-generated files, to be solved upstream in Menhir
 
 COQCOPTS ?= \
-  -w -undeclared-scope \
   -w -unused-pattern-matching-variable \
   -w -deprecated-ident-entry
 
diff --git a/MenhirLib/Interpreter.v b/MenhirLib/Interpreter.v
index 158bba9f..922d6656 100644
--- a/MenhirLib/Interpreter.v
+++ b/MenhirLib/Interpreter.v
@@ -84,8 +84,8 @@ CoInductive buffer : Type :=
   Buf_cons { buf_head : token; buf_tail : buffer }.
 
 (* Note: Coq 8.12.0 wants a Declare Scope command,
-   but this breaks compatibility with Coq < 8.10.
-   Declare Scope buffer_scope. *)
+   but this breaks compatibility with Coq < 8.10. *)
+Declare Scope buffer_scope.
 Delimit Scope buffer_scope with buf.
 Bind Scope buffer_scope with buffer.
 
diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index c5f4032e..0b5b01b8 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -96,6 +96,7 @@ Coercion preg_of_iregsp: iregsp >-> preg.
 
 (** Conventional name for return address ([RA]) *)
 
+Declare Scope asm.
 Notation "'RA'" := X30 (only parsing) : asm.
 
 (** The instruction set.  Most instructions correspond exactly to
diff --git a/arm/Asm.v b/arm/Asm.v
index 8c902074..f0dd347f 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -94,6 +94,7 @@ Module Pregmap := EMap(PregEq).
 
 (** Conventional names for stack pointer ([SP]) and return address ([RA]) *)
 
+Declare Scope asm.
 Notation "'SP'" := IR13 (only parsing) : asm.
 Notation "'RA'" := IR14 (only parsing) : asm.
 
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.
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 52037ac0..f02da0c8 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -25,6 +25,8 @@ Local Open Scope list_scope.
 
 (** Error monad with options or lists *)
 
+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.
@@ -45,6 +47,8 @@ Notation " 'check' A ; B" := (if A then B else None)
   (at level 200, A at level 100, B at level 200)
   : option_monad_scope.
 
+Declare Scope list_monad_scope.
+
 Notation "'do' X <- A ; B" := (match A with Some X => B | None => nil end)
   (at level 200, X ident, A at level 100, B at level 200)
   : list_monad_scope.
@@ -745,6 +749,8 @@ Definition incontext2 {A1 A2 B: Type}
                      (ctx2: A2 -> B) (ll2: reducts A2) : reducts B :=
   incontext ctx1 ll1 ++ incontext ctx2 ll2.
 
+Declare Scope reducts_monad_scope.
+
 Notation "'do' X <- A ; B" := (match A with Some X => B | None => stuck end)
   (at level 200, X ident, A at level 100, B at level 200)
   : reducts_monad_scope.
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index bb1dbe38..cf5dd6d1 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -55,6 +55,7 @@ Definition bind {A B: Type} (x: mon A) (f: A -> mon B) : mon B :=
 Definition bind2 {A B C: Type} (x: mon (A * B)) (f: A -> B -> mon C) : mon C :=
   bind x (fun p => f (fst p) (snd p)).
 
+Declare Scope gensym_monad_scope.
 Notation "'do' X <- A ; B" := (bind A (fun X => B))
    (at level 200, X ident, A at level 100, B at level 200)
    : gensym_monad_scope.
diff --git a/common/Errors.v b/common/Errors.v
index bf72f12b..d9158165 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -67,6 +67,8 @@ Definition bind2 (A B C: Type) (f: res (A * B)) (g: A -> B -> res C) : res C :=
 
 (** The [do] notation, inspired by Haskell's, keeps the code readable. *)
 
+Declare Scope error_monad_scope.
+
 Notation "'do' X <- A ; B" := (bind A (fun X => B))
  (at level 200, X ident, A at level 100, B at level 200)
  : error_monad_scope.
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index f424a69d..1c5bf4ff 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -39,9 +39,9 @@ Require Import Zwf.
 Require Import Axioms Coqlib Errors Maps AST Linking.
 Require Import Integers Floats Values Memory.
 
+Declare Scope pair_scope.
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
-
 Local Open Scope pair_scope.
 Local Open Scope error_monad_scope.
 
diff --git a/common/Linking.v b/common/Linking.v
index 4ef83d42..54d1628e 100644
--- a/common/Linking.v
+++ b/common/Linking.v
@@ -862,6 +862,8 @@ Inductive Passes: Language -> Language -> Type :=
   | pass_nil: forall l, Passes l l
   | pass_cons: forall l1 l2 l3, Pass l1 l2 -> Passes l2 l3 -> Passes l1 l3.
 
+Declare Scope linking_scope.
+
 Infix ":::" := pass_cons (at level 60, right associativity) : linking_scope.
 
 (** The pass corresponding to the composition of a list of passes. *)
diff --git a/common/Separation.v b/common/Separation.v
index f41d94c3..2ba6e77b 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -54,6 +54,7 @@ Record massert : Type := {
   m_valid: forall m b ofs, m_pred m -> m_footprint b ofs -> Mem.valid_block m b
 }.
 
+Declare Scope sep_scope.
 Notation "m |= p" := (m_pred p m) (at level 74, no associativity) : sep_scope.
 
 (** Implication and logical equivalence between memory predicates *)
diff --git a/common/Smallstep.v b/common/Smallstep.v
index 487e7a80..3cbd8934 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -552,6 +552,8 @@ Definition Semantics {state funtype vartype: Type}
 
 (** Handy notations. *)
 
+Declare Scope smallstep_scope.
+
 Notation " 'Step' L " := (step L (globalenv L)) (at level 1) : smallstep_scope.
 Notation " 'Star' L " := (star (step L) (globalenv L)) (at level 1) : smallstep_scope.
 Notation " 'Plus' L " := (plus (step L) (globalenv L)) (at level 1) : smallstep_scope.
diff --git a/export/Clightdefs.v b/export/Clightdefs.v
index dc4e3491..3a9da8f6 100644
--- a/export/Clightdefs.v
+++ b/export/Clightdefs.v
@@ -49,6 +49,8 @@ Definition mkprogram (types: list composite_definition)
 
 (** ** Notations *)
 
+Declare Scope clight_scope.
+
 Module ClightNotations.
 
 (** A convenient notation [$ "ident"] to force evaluation of
diff --git a/export/Csyntaxdefs.v b/export/Csyntaxdefs.v
index 84ce9f3a..67bc7f51 100644
--- a/export/Csyntaxdefs.v
+++ b/export/Csyntaxdefs.v
@@ -49,6 +49,8 @@ Definition mkprogram (types: list composite_definition)
 
 (** ** Notations *)
 
+Declare Scope csyntax_scope.
+
 Module CsyntaxNotations.
 
 (** A convenient notation [$ "ident"] to force evaluation of
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 6b1f2232..ea6f5c92 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -87,6 +87,7 @@ Module Pregmap := EMap(PregEq).
 
 (** Conventional names for stack pointer ([SP]) and return address ([RA]) *)
 
+Declare Scope asm.
 Notation "'SP'" := GPR1 (only parsing) : asm.
 Notation "'RA'" := LR (only parsing) : asm.
 
diff --git a/riscV/Asm.v b/riscV/Asm.v
index cbe3476a..15c3dab4 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -93,6 +93,7 @@ Module Pregmap := EMap(PregEq).
 
 (** Conventional names for stack pointer ([SP]) and return address ([RA]). *)
 
+Declare Scope asm.
 Notation "'SP'" := X2 (only parsing) : asm.
 Notation "'RA'" := X1 (only parsing) : asm.
 
diff --git a/x86/Asm.v b/x86/Asm.v
index b9c4817a..64a835e1 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -312,6 +312,7 @@ Module Pregmap := EMap(PregEq).
 Definition regset := Pregmap.t val.
 Definition genv := Genv.t fundef unit.
 
+Declare Scope asm.
 Notation "a # b" := (a b) (at level 1, only parsing) : asm.
 Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.