From 51c497b2e5a2b09788f2cf05f414634b037f52bf Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 23 Apr 2019 15:00:41 +0200 Subject: lib/Coqlib.v: remove defns about multiplication, division, modulus Instead, use definitions and lemmas from the Coq standard library (ZArith, Znumtheory). --- common/Memdata.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'common/Memdata.v') diff --git a/common/Memdata.v b/common/Memdata.v index 307a02db..c53f0e5d 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -258,14 +258,14 @@ Lemma decode_encode_int_4: forall x, Int.repr (decode_int (encode_int 4 (Int.unsigned x))) = x. Proof. intros. rewrite decode_encode_int. transitivity (Int.repr (Int.unsigned x)). - decEq. apply Zmod_small. apply Int.unsigned_range. apply Int.repr_unsigned. + decEq. apply Z.mod_small. apply Int.unsigned_range. apply Int.repr_unsigned. Qed. Lemma decode_encode_int_8: forall x, Int64.repr (decode_int (encode_int 8 (Int64.unsigned x))) = x. Proof. intros. rewrite decode_encode_int. transitivity (Int64.repr (Int64.unsigned x)). - decEq. apply Zmod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned. + decEq. apply Z.mod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned. Qed. (** A length-[n] encoding depends only on the low [8*n] bits of the integer. *) -- cgit