From 103aa7074a9dd3b1bcb2864d52c89292a2ab7bff Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 19 Sep 2022 16:28:06 +0200 Subject: 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. --- cfrontend/Cexec.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'cfrontend/Cexec.v') 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. -- cgit