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 /backend/Asmexpandaux.ml | |
parent | de830925c012c8c725ffc59b64883f4cae3586bb (diff) | |
download | compcert-4136f69ea08425cff59c463b10a5db73b3dfc59a.tar.gz compcert-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 'backend/Asmexpandaux.ml')
0 files changed, 0 insertions, 0 deletions