From cf56eea4e093f25a5c01ccac5ede2a69b568af7a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Mar 2020 20:16:16 +0100 Subject: load_store_away --- backend/CSE2proof.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'backend/CSE2proof.v') 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. -- cgit