diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2022-09-19 16:28:06 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-09-19 16:28:06 +0200 |
commit | 103aa7074a9dd3b1bcb2864d52c89292a2ab7bff (patch) | |
tree | c2b8e6f224daa9afe54a998b8c7e832b33c5c0b2 /cfrontend | |
parent | b816d696733c96fdc62428e43c4a4a1f5a09b47b (diff) | |
download | compcert-103aa7074a9dd3b1bcb2864d52c89292a2ab7bff.tar.gz compcert-103aa7074a9dd3b1bcb2864d52c89292a2ab7bff.zip |
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.
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cexec.v | 6 | ||||
-rw-r--r-- | cfrontend/SimplExpr.v | 1 |
2 files changed, 7 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. 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. |