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). --- cfrontend/Cminorgenproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index ffafc5d2..5acb996d 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -923,7 +923,7 @@ Remark inj_offset_aligned_block: Mem.inj_offset_aligned (align stacksize (block_alignment sz)) sz. Proof. intros; red; intros. - apply Zdivides_trans with (block_alignment sz). + apply Z.divide_trans with (block_alignment sz). unfold align_chunk. unfold block_alignment. generalize Z.divide_1_l; intro. generalize Z.divide_refl; intro. -- cgit