From 1e0d5047d2272fdeb06391d1c5fa4e0472be2365 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Mon, 29 Jun 2020 21:29:32 +0100
Subject: Eliminate memory bounds assumption!

---
 src/common/IntegerExtra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/common')

diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index 8df70d9..7d3156b 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -143,7 +143,7 @@ Module PtrofsExtra.
   Lemma divu_unsigned :
     forall x y,
       0 < Ptrofs.unsigned y ->
-      Ptrofs.unsigned x < Ptrofs.max_unsigned ->
+      Ptrofs.unsigned x <= Ptrofs.max_unsigned ->
       Ptrofs.unsigned (Ptrofs.divu x y) = Ptrofs.unsigned x / Ptrofs.unsigned y.
   Proof.
     intros.
@@ -154,7 +154,7 @@ Module PtrofsExtra.
     apply Ptrofs.unsigned_range.
     apply Z.div_le_upper_bound; auto.
     eapply Z.le_trans.
-    apply Z.lt_le_incl. exact H0.
+    exact H0.
     rewrite Z.mul_comm.
     apply Z.le_mul_diag_r; simplify; lia.
   Qed.
-- 
cgit