diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-15 16:24:13 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-15 16:24:13 +0000 |
| commit | f774d5f2d604f747e72e2d3bb56cc3f90090e2dd (patch) | |
| tree | 05a5bcfc207c67f58575fa7b61787c0c9dbe8215 /arm/Asmgenproof.v | |
| parent | f1ceca440c0322001abe6c5de79bd4bc309fc002 (diff) | |
| download | compcert-kvx-f774d5f2d604f747e72e2d3bb56cc3f90090e2dd.tar.gz compcert-kvx-f774d5f2d604f747e72e2d3bb56cc3f90090e2dd.zip | |
Pointers one past
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/Asmgenproof.v')
| -rw-r--r-- | arm/Asmgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index b0598e90..365917cb 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -348,7 +348,7 @@ Remark loadimm_label: forall r n k, find_label lbl (loadimm r n k) = find_label lbl k. Proof. intros. unfold loadimm. - destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n)))); + destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.not n)))); auto with labels. Qed. Hint Rewrite loadimm_label: labels. @@ -357,7 +357,7 @@ Remark addimm_label: forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k. Proof. intros; unfold addimm. - destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n)))); + destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))); auto with labels. Qed. Hint Rewrite addimm_label: labels. |