aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/SimplExpr.v
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2022-09-19 16:28:06 +0200
committerGitHub <noreply@github.com>2022-09-19 16:28:06 +0200
commit103aa7074a9dd3b1bcb2864d52c89292a2ab7bff (patch)
treec2b8e6f224daa9afe54a998b8c7e832b33c5c0b2 /cfrontend/SimplExpr.v
parentb816d696733c96fdc62428e43c4a4a1f5a09b47b (diff)
downloadcompcert-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/SimplExpr.v')
-rw-r--r--cfrontend/SimplExpr.v1
1 files changed, 1 insertions, 0 deletions
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.