diff options
author | Frédéric Besson <frederic.besson@inria.fr> | 2019-10-30 09:38:01 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-10-30 09:38:01 +0100 |
commit | a0844a9b6eb88f9e75f7305e8d1505cf502fb81a (patch) | |
tree | 3e41306b371d2fcab33a6bf6fa057d139f81e026 /cparser/Cflow.mli | |
parent | 1c1a4d86a22dd04fc92e61d4bd5c35e047c8b772 (diff) | |
download | compcert-a0844a9b6eb88f9e75f7305e8d1505cf502fb81a.tar.gz compcert-a0844a9b6eb88f9e75f7305e8d1505cf502fb81a.zip |
More robust proof of `size_and` (#320)
The proposed proof only uses `zify` for closing the goal. This is
needed for Coq PR #10982 which changes the inner working of `zify`.
Diffstat (limited to 'cparser/Cflow.mli')
0 files changed, 0 insertions, 0 deletions