From 18900d3c0da37c4dc7079749f84517fb7456e551 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 16 Aug 2018 17:32:32 +0100
Subject: Add the type an expression was checked against to tannots, and use
 for Coq Tweak extra Coq files to match. Tweak early return rewrite to use
 declared return type, which can always be put into an E_cast.

---
 mips/mips_extras.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'mips/mips_extras.v')

diff --git a/mips/mips_extras.v b/mips/mips_extras.v
index 626b4109..51856d9e 100644
--- a/mips/mips_extras.v
+++ b/mips/mips_extras.v
@@ -162,10 +162,12 @@ Require DecimalString.
 Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z).
 
 
-Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * size ÷ 8).
+Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * (8 * size ÷ 8) ÷ 8).
 intros.
 rewrite Z.mul_comm.
 rewrite Z.quot_mul; auto with zarith.
+rewrite Z.mul_comm with (m := size).
+rewrite Z.quot_mul; auto with zarith.
 Qed.
 Hint Resolve MEMr_wrapper_lemma : sail.
 
-- 
cgit v1.2.3