diff options
Diffstat (limited to 'backend/Inliningproof.v')
| -rw-r--r-- | backend/Inliningproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 2dcb8956..181f40bf 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -755,13 +755,13 @@ Proof. assert (2 <= sz -> (2 | n)). intros. destruct (zle sz 1). omegaContradiction. destruct (zle sz 2). auto. - destruct (zle sz 4). apply Zdivides_trans with 4; auto. exists 2; auto. - apply Zdivides_trans with 8; auto. exists 4; auto. + destruct (zle sz 4). apply Z.divide_trans with 4; auto. exists 2; auto. + apply Z.divide_trans with 8; auto. exists 4; auto. assert (4 <= sz -> (4 | n)). intros. destruct (zle sz 1). omegaContradiction. destruct (zle sz 2). omegaContradiction. destruct (zle sz 4). auto. - apply Zdivides_trans with 8; auto. exists 2; auto. + apply Z.divide_trans with 8; auto. exists 2; auto. assert (8 <= sz -> (8 | n)). intros. destruct (zle sz 1). omegaContradiction. destruct (zle sz 2). omegaContradiction. @@ -1249,7 +1249,7 @@ Proof. eapply external_call_nextblock; eauto. auto. auto. -- (* return fron noninlined function *) +- (* return from noninlined function *) inv MS0. + (* normal case *) left; econstructor; split. |