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 /Makefile | |
| 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 'Makefile')
| -rw-r--r-- | Makefile | 4 |
1 files changed, 0 insertions, 4 deletions
@@ -44,9 +44,6 @@ endif # Notes on silenced Coq warnings: # -# undeclared-scope: -# warning introduced in 8.12 -# suggested change (use `Declare Scope`) supported since 8.12 # unused-pattern-matching-variable: # warning introduced in 8.13 # the code rewrite that avoids the warning is not desirable @@ -58,7 +55,6 @@ endif # triggered by Menhir-generated files, to be solved upstream in Menhir COQCOPTS ?= \ - -w -undeclared-scope \ -w -unused-pattern-matching-variable \ -w -deprecated-ident-entry |