aboutsummaryrefslogtreecommitdiffstats
path: root/arm/ConstpropOpproof.v
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-12-01 10:00:05 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-12-01 10:00:05 +0100
commit442e82e6ffc6958192f73382d2270e926ead9c80 (patch)
tree24409429d6ab33acaa16d30bac07558d5204b7aa /arm/ConstpropOpproof.v
parentd4070c456e71b6edfc9b65e5ec837370fea8e9d0 (diff)
downloadcompcert-kvx-442e82e6ffc6958192f73382d2270e926ead9c80.tar.gz
compcert-kvx-442e82e6ffc6958192f73382d2270e926ead9c80.zip
Added simple div_one Theorem variants.
Diffstat (limited to 'arm/ConstpropOpproof.v')
0 files changed, 0 insertions, 0 deletions