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/Separation.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'common/Separation.v') diff --git a/common/Separation.v b/common/Separation.v index a9642d72..1493b535 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -702,7 +702,7 @@ Proof. - intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). omega. - intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. xomega. -- red; intros. apply Zdivides_trans with 8; auto. +- red; intros. apply Z.divide_trans with 8; auto. exists (8 / align_chunk chunk). destruct chunk; reflexivity. - intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. - intros (j' & INJ' & J1 & J2 & J3). -- cgit