aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Integers.v
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-01-14 11:05:36 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-01-14 11:05:36 +0100
commit9c6fac6cd52b824aaefac66089bf5c71e27845be (patch)
treea3724f9a2109d6de563606a231ad7c59a5b693de /lib/Integers.v
parent804e8174a944e3d8983c077502e57113ecdda6dd (diff)
downloadcompcert-kvx-9c6fac6cd52b824aaefac66089bf5c71e27845be.tar.gz
compcert-kvx-9c6fac6cd52b824aaefac66089bf5c71e27845be.zip
rv32: 3-instruction signed divide-by-two sequence (as opposed to 4)
Diffstat (limited to 'lib/Integers.v')
0 files changed, 0 insertions, 0 deletions