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 /.gitignore | |
| 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 '.gitignore')
0 files changed, 0 insertions, 0 deletions