diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-02 20:16:16 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-02 20:16:16 +0100 |
| commit | cf56eea4e093f25a5c01ccac5ede2a69b568af7a (patch) | |
| tree | 59c433f4c1908cceb8b74f9dbc14d2752538a408 /backend/CSE2proof.v | |
| parent | f7ea436ac282b6a4a8ddb2281b6e1d86eee46286 (diff) | |
| download | compcert-kvx-cf56eea4e093f25a5c01ccac5ede2a69b568af7a.tar.gz compcert-kvx-cf56eea4e093f25a5c01ccac5ede2a69b568af7a.zip | |
load_store_away
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 6d5496fd..c6bb00dd 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -783,7 +783,8 @@ Section MEMORY_WRITE. repeat rewrite andb_true_iff in SWAP. repeat rewrite orb_true_iff in SWAP. repeat rewrite Z.leb_le in SWAP. - apply load_store_away1; intuition. + apply load_store_away1. + all: tauto. Qed. End MEMORY_WRITE. |