diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-09-17 15:11:48 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-09-17 15:11:48 +0200 |
commit | 322f3c865341fdfd5d22ab885b2934a5213ddbaa (patch) | |
tree | 70912af2a6cd75d72b57172d910d71a6abd2d447 /lib/Heaps.v | |
parent | 6b87278c399332f67a4b40958ea2386bb3c1c66e (diff) | |
download | compcert-322f3c865341fdfd5d22ab885b2934a5213ddbaa.tar.gz compcert-322f3c865341fdfd5d22ab885b2934a5213ddbaa.zip |
Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpy
Inline directives in extraction.v make the Caml output efficient and almost nice.
Diffstat (limited to 'lib/Heaps.v')
0 files changed, 0 insertions, 0 deletions