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). --- backend/Inliningproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/Inliningproof.v') diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 2dcb8956..45051bcf 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -755,13 +755,13 @@ Proof. assert (2 <= sz -> (2 | n)). intros. destruct (zle sz 1). omegaContradiction. destruct (zle sz 2). auto. - destruct (zle sz 4). apply Zdivides_trans with 4; auto. exists 2; auto. - apply Zdivides_trans with 8; auto. exists 4; auto. + destruct (zle sz 4). apply Z.divide_trans with 4; auto. exists 2; auto. + apply Z.divide_trans with 8; auto. exists 4; auto. assert (4 <= sz -> (4 | n)). intros. destruct (zle sz 1). omegaContradiction. destruct (zle sz 2). omegaContradiction. destruct (zle sz 4). auto. - apply Zdivides_trans with 8; auto. exists 2; auto. + apply Z.divide_trans with 8; auto. exists 2; auto. assert (8 <= sz -> (8 | n)). intros. destruct (zle sz 1). omegaContradiction. destruct (zle sz 2). omegaContradiction. -- cgit