diff options
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. |