diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-08 08:35:29 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-08 08:35:29 +0100 |
commit | 177c8fbc523a171e8c8470fa675f9a69ef7f99de (patch) | |
tree | f54d8315891bec2f741545991f420dd4407bccc0 /test/regression/volatile2.c | |
parent | 44b63eb13151ca5c3e83ee6a9e7eb6c0049c3758 (diff) | |
download | compcert-177c8fbc523a171e8c8470fa675f9a69ef7f99de.tar.gz compcert-177c8fbc523a171e8c8470fa675f9a69ef7f99de.zip |
Adapt proofs to future handling of literal constants in Coq.
This commit is mainly a squash of the relevant compatibility commits from
Flocq's master. Most of the changes are meant to make the proofs oblivious
to the way constants such as 0, 1, 2, and -1 are represented.
Diffstat (limited to 'test/regression/volatile2.c')
0 files changed, 0 insertions, 0 deletions