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 /common/Globalenvs.v | |
| 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 'common/Globalenvs.v')
| -rw-r--r-- | common/Globalenvs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index f424a69d..1c5bf4ff 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -39,9 +39,9 @@ Require Import Zwf. Require Import Axioms Coqlib Errors Maps AST Linking. Require Import Integers Floats Values Memory. +Declare Scope pair_scope. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. - Local Open Scope pair_scope. Local Open Scope error_monad_scope. |