diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-22 19:53:06 +0200 |
| commit | 8d5c6bb8f0cac1339dec7b730997ee30b1517073 (patch) | |
| tree | 3ffd8bcb28a88ae4ff51989aed37b0ad2cb676b2 /common/Separation.v | |
| parent | 0f210f622a4609811959f4450f770c61f5eb6532 (diff) | |
| download | compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.tar.gz compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.zip | |
Remove coq warnings (#28)
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
Diffstat (limited to 'common/Separation.v')
| -rw-r--r-- | common/Separation.v | 8 |
1 files changed, 4 insertions, 4 deletions
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', |