aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asmgenproof.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2017-08-17 11:18:19 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2017-08-17 11:18:19 +0200
commit82c4547961d567003a83d6c489e06f1271e80a7f (patch)
tree42241cb1b92ab2c97ab12e1d696cd26c449b8a95 /arm/Asmgenproof.v
parentc9d01df3577a23e20abbe934f6f36f17dbbb82cd (diff)
downloadcompcert-kvx-82c4547961d567003a83d6c489e06f1271e80a7f.tar.gz
compcert-kvx-82c4547961d567003a83d6c489e06f1271e80a7f.zip
Asmgenproof0: some more useful lemmas
Next commit uses those lemmas in the ARM port.
Diffstat (limited to 'arm/Asmgenproof.v')
0 files changed, 0 insertions, 0 deletions