diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-09-11 16:16:33 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-09-11 16:16:33 +0200 |
commit | f3bdf0c70faa9e69359bd06b78570c60a569a7cb (patch) | |
tree | 2e776de2f8065803ab47d881e1aeb19f0165b20b /arm/ValueAOp.v | |
parent | 7601fb5e792a5305336e5cda9794c4041d053b95 (diff) | |
download | compcert-f3bdf0c70faa9e69359bd06b78570c60a569a7cb.tar.gz compcert-f3bdf0c70faa9e69359bd06b78570c60a569a7cb.zip |
Asmgenproof1: useless unfolding in proof scripts causing "omega" to fail
"omega" fails in Coq 8.7, but not in 8.8 and later.
Diffstat (limited to 'arm/ValueAOp.v')
0 files changed, 0 insertions, 0 deletions