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.

1 files changed, 6 insertions, 0 deletions

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.