diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 08:30:14 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 08:30:14 +0200 |
| commit | d5b86a98560c36fbcb3ab8d2698e09147acda512 (patch) | |
| tree | f3ab850a1620fa5d3dbbe439998d09de8e0d817d /arm/Asmgenproof.v | |
| parent | ea2d6b70ed06c60dba9ba81cf53883c85fb92068 (diff) | |
| parent | 3872ce9f9806d9af334b1fde092145edf664d170 (diff) | |
| download | compcert-d5b86a98560c36fbcb3ab8d2698e09147acda512.tar.gz compcert-d5b86a98560c36fbcb3ab8d2698e09147acda512.zip | |
Merge branch 'master' into add-file
Diffstat (limited to 'arm/Asmgenproof.v')
| -rw-r--r-- | arm/Asmgenproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 5bd2b54f..431743c6 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -166,11 +166,11 @@ Proof. intros. unfold loadimm. set (l1 := length (decompose_int n)). set (l2 := length (decompose_int (Int.not n))). - destruct (NPeano.leb l1 1%nat). TailNoLabel. - destruct (NPeano.leb l2 1%nat). TailNoLabel. + destruct (Nat.leb l1 1%nat). TailNoLabel. + destruct (Nat.leb l2 1%nat). TailNoLabel. destruct (thumb tt). unfold loadimm_thumb. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero); TailNoLabel. - destruct (NPeano.leb l1 l2); auto with labels. + destruct (Nat.leb l1 l2); auto with labels. Qed. Hint Resolve loadimm_label: labels. @@ -179,7 +179,7 @@ Remark addimm_label: Proof. intros; unfold addimm. destruct (Int.ltu (Int.repr (-256)) n). TailNoLabel. - destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))); + destruct (Nat.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))); auto with labels. Qed. Hint Resolve addimm_label: labels. |