From 51c497b2e5a2b09788f2cf05f414634b037f52bf Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
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).
---
 arm/Op.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'arm/Op.v')

diff --git a/arm/Op.v b/arm/Op.v
index 60c214d0..8e1cd367 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -532,7 +532,7 @@ Lemma mk_shift_amount_eq:
   forall n, Int.ltu n Int.iwordsize = true -> s_amount (mk_shift_amount n) = n.
 Proof.
   intros; simpl. unfold Int.modu. transitivity (Int.repr (Int.unsigned n)).
-  decEq. apply Zmod_small. apply Int.ltu_inv; auto.
+  decEq. apply Z.mod_small. apply Int.ltu_inv; auto.
   apply Int.repr_unsigned.
 Qed.
 
-- 
cgit