diff options
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', |