diff options
Diffstat (limited to 'backend/Inliningproof.v')
| -rw-r--r-- | backend/Inliningproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 2dcb8956..45051bcf 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. |