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 | |
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')
-rw-r--r-- | common/Errors.v | 2 | ||||
-rw-r--r-- | common/Globalenvs.v | 2 | ||||
-rw-r--r-- | common/Linking.v | 2 | ||||
-rw-r--r-- | common/Separation.v | 1 | ||||
-rw-r--r-- | common/Smallstep.v | 2 |
5 files changed, 8 insertions, 1 deletions
diff --git a/common/Errors.v b/common/Errors.v index bf72f12b..d9158165 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -67,6 +67,8 @@ Definition bind2 (A B C: Type) (f: res (A * B)) (g: A -> B -> res C) : res C := (** The [do] notation, inspired by Haskell's, keeps the code readable. *) +Declare Scope error_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) : error_monad_scope. 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. diff --git a/common/Linking.v b/common/Linking.v index 4ef83d42..54d1628e 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -862,6 +862,8 @@ Inductive Passes: Language -> Language -> Type := | pass_nil: forall l, Passes l l | pass_cons: forall l1 l2 l3, Pass l1 l2 -> Passes l2 l3 -> Passes l1 l3. +Declare Scope linking_scope. + Infix ":::" := pass_cons (at level 60, right associativity) : linking_scope. (** The pass corresponding to the composition of a list of passes. *) diff --git a/common/Separation.v b/common/Separation.v index f41d94c3..2ba6e77b 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -54,6 +54,7 @@ Record massert : Type := { m_valid: forall m b ofs, m_pred m -> m_footprint b ofs -> Mem.valid_block m b }. +Declare Scope sep_scope. Notation "m |= p" := (m_pred p m) (at level 74, no associativity) : sep_scope. (** Implication and logical equivalence between memory predicates *) diff --git a/common/Smallstep.v b/common/Smallstep.v index 487e7a80..3cbd8934 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -552,6 +552,8 @@ Definition Semantics {state funtype vartype: Type} (** Handy notations. *) +Declare Scope smallstep_scope. + Notation " 'Step' L " := (step L (globalenv L)) (at level 1) : smallstep_scope. Notation " 'Star' L " := (star (step L) (globalenv L)) (at level 1) : smallstep_scope. Notation " 'Plus' L " := (plus (step L) (globalenv L)) (at level 1) : smallstep_scope. |