aboutsummaryrefslogtreecommitdiffstats
path: root/common/Smallstep.v
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2022-09-19 16:28:06 +0200
committerGitHub <noreply@github.com>2022-09-19 16:28:06 +0200
commit103aa7074a9dd3b1bcb2864d52c89292a2ab7bff (patch)
treec2b8e6f224daa9afe54a998b8c7e832b33c5c0b2 /common/Smallstep.v
parentb816d696733c96fdc62428e43c4a4a1f5a09b47b (diff)
downloadcompcert-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/Smallstep.v')
-rw-r--r--common/Smallstep.v2
1 files changed, 2 insertions, 0 deletions
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.