aboutsummaryrefslogtreecommitdiffstats
path: root/x86
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2021-01-21 16:54:40 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2021-01-21 17:17:34 +0100
commit25483cf1acce8695a438f4f2164b09fb1ecd9d2e (patch)
treed7c96d261975a0b4bc5bbce4209a9e1e19b13e2f /x86
parentfc82b6c80fd3feeb4ef9478e6faa16b5b1104593 (diff)
downloadcompcert-kvx-25483cf1acce8695a438f4f2164b09fb1ecd9d2e.tar.gz
compcert-kvx-25483cf1acce8695a438f4f2164b09fb1ecd9d2e.zip
Silence some new warnings of Coq 8.13
Either because the code change that would silence the warning is not desirable, or because it would break compatibility with earlier versions of Coq. Explain the silenced warnings as comments in the Makefile.
Diffstat (limited to 'x86')
0 files changed, 0 insertions, 0 deletions