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 /powerpc | |
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 'powerpc')
-rw-r--r-- | powerpc/Asm.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 6b1f2232..ea6f5c92 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -87,6 +87,7 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]) *) +Declare Scope asm. Notation "'SP'" := GPR1 (only parsing) : asm. Notation "'RA'" := LR (only parsing) : asm. |