From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 22 Sep 2017 19:50:52 +0200 Subject: Remove coq warnings (#28) Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts. --- common/Separation.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'common/Separation.v') diff --git a/common/Separation.v b/common/Separation.v index c27148aa..a9642d72 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -680,7 +680,7 @@ Lemma alloc_parallel_rule: Mem.alloc m2 0 sz2 = (m2', b2) -> (8 | delta) -> lo = delta -> - hi = delta + Zmax 0 sz1 -> + hi = delta + Z.max 0 sz1 -> 0 <= sz2 <= Ptrofs.max_unsigned -> 0 <= delta -> hi <= sz2 -> exists j', @@ -740,7 +740,7 @@ Lemma free_parallel_rule: m2 |= range b2 0 lo ** range b2 hi sz2 ** minjection j m1 ** P -> Mem.free m1 b1 0 sz1 = Some m1' -> j b1 = Some (b2, delta) -> - lo = delta -> hi = delta + Zmax 0 sz1 -> + lo = delta -> hi = delta + Z.max 0 sz1 -> exists m2', Mem.free m2 b2 0 sz2 = Some m2' /\ m2' |= minjection j m1' ** P. @@ -841,7 +841,7 @@ Proof. - eauto. - destruct (j b1) as [[b0 delta0]|] eqn:JB1. + erewrite H in H1 by eauto. inv H1. eauto. -+ exploit H0; eauto. intros (X & Y). elim Y. apply Plt_le_trans with bound; auto. ++ exploit H0; eauto. intros (X & Y). elim Y. apply Pos.lt_le_trans with bound; auto. - eauto. - eauto. - eauto. @@ -890,7 +890,7 @@ Lemma alloc_parallel_rule_2: Mem.alloc m2 0 sz2 = (m2', b2) -> (8 | delta) -> lo = delta -> - hi = delta + Zmax 0 sz1 -> + hi = delta + Z.max 0 sz1 -> 0 <= sz2 <= Ptrofs.max_unsigned -> 0 <= delta -> hi <= sz2 -> exists j', -- cgit