diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-05 16:01:46 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-08-05 18:33:17 +0200 |
| commit | 4136f69ea08425cff59c463b10a5db73b3dfc59a (patch) | |
| tree | fd5744aa607522fd096038c41e016d2fe5e89a29 /x86/CBuiltins.ml | |
| parent | de830925c012c8c725ffc59b64883f4cae3586bb (diff) | |
| download | compcert-kvx-4136f69ea08425cff59c463b10a5db73b3dfc59a.tar.gz compcert-kvx-4136f69ea08425cff59c463b10a5db73b3dfc59a.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/CBuiltins.ml')
0 files changed, 0 insertions, 0 deletions