diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-05 16:01:46 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:37:28 +0200 |
| commit | f19b7fd7a0b87d7fcce021a264f9b95c43a24a09 (patch) | |
| tree | fd5744aa607522fd096038c41e016d2fe5e89a29 /x86 | |
| parent | efb5f52493345a1e17cc10b56023dfe00beb6074 (diff) | |
| download | compcert-f19b7fd7a0b87d7fcce021a264f9b95c43a24a09.tar.gz compcert-f19b7fd7a0b87d7fcce021a264f9b95c43a24a09.zip | |
Coq 8.10 compatibility: (temporarily) silence new warning
The "undeclared-scope" warning fires when we use a "notation" scope
before having declared it. This is a good thing, except that
the "Declare Scope" vernacular that declares a scope was introduced
in Coq 8.10 and is not available in earlier versions.
Hence there is no way to avoid triggering the warning yet remain
compatible with pre-8.10 Coq versions.
This commit silences the warning. It will have to revisited when
Coq 8.10 is the oldest version of Coq we support in CompCert.
Diffstat (limited to 'x86')
0 files changed, 0 insertions, 0 deletions