diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-26 17:35:58 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-10-03 18:43:34 +0200 |
| commit | cc3f0838d115830b2f2fba55ff8c53c212db6979 (patch) | |
| tree | 519b9d1631f2d65ce50db239e28583ae2ac801dd /configure | |
| parent | 2c46ae4bd8f9f49554daa31988fd98793cc5601e (diff) | |
| download | compcert-kvx-cc3f0838d115830b2f2fba55ff8c53c212db6979.tar.gz compcert-kvx-cc3f0838d115830b2f2fba55ff8c53c212db6979.zip | |
Selectively turn some Coq 8.14 warnings off
Warning "deprecated hint rewrite without locality" cannot be addressed:
the suggested fix (qualify with Global or Local or [#export])
is not supported by Coq 8.11 to 8.13 !
Warning "deprecated instance without locality" is turned off
for generated file cparser/Parser.v only.
Menhir needs to be changed so as to generate the `Global` modifier
that would silence this warning.
Diffstat (limited to 'configure')
0 files changed, 0 insertions, 0 deletions