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. --- backend/Allocation.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backend/Allocation.v') 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. -- cgit