diff options
| author | Vincent Laporte <vbgl@users.noreply.github.com> | 2019-02-12 19:52:15 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-02-12 19:52:15 +0100 |
| commit | 873c62128ea8aeb2a26384be2be09b9324b9ed9c (patch) | |
| tree | 2694dc9aa9028568557aa84f10cdcc893b53fafe /riscV | |
| parent | 0b3193b0019373305aec293362956bdb24cbb9a0 (diff) | |
| download | compcert-873c62128ea8aeb2a26384be2be09b9324b9ed9c.tar.gz compcert-873c62128ea8aeb2a26384be2be09b9324b9ed9c.zip | |
Make the checker happy (#272)
Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
Diffstat (limited to 'riscV')
0 files changed, 0 insertions, 0 deletions