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. --- powerpc/Asm.v | 1 + 1 file changed, 1 insertion(+) (limited to 'powerpc/Asm.v') 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. -- cgit