diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-08 14:43:57 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-08 14:43:57 +0200 |
| commit | e73d5db97cdb22cce2ee479469f62af3c4b6264a (patch) | |
| tree | 035d31018c2abec698eb49a205c60bbf5c24ba0d /arm/Asmgen.v | |
| parent | db2445b3b745abd1a26f5a832a29ca269c725277 (diff) | |
| download | compcert-kvx-e73d5db97cdb22cce2ee479469f62af3c4b6264a.tar.gz compcert-kvx-e73d5db97cdb22cce2ee479469f62af3c4b6264a.zip | |
Port to Coq 8.5pl2
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
Diffstat (limited to 'arm/Asmgen.v')
| -rw-r--r-- | arm/Asmgen.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 7b3f2fdc..90d3b189 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -173,13 +173,13 @@ Definition loadimm (r: ireg) (n: int) (k: code) := let d2 := decompose_int (Int.not n) in let l1 := List.length d1 in let l2 := List.length d2 in - if NPeano.leb l1 1%nat then + if Nat.leb l1 1%nat then Pmov r (SOimm n) :: k - else if NPeano.leb l2 1%nat then + else if Nat.leb l2 1%nat then Pmvn r (SOimm (Int.not n)) :: k else if thumb tt then loadimm_thumb r n k - else if NPeano.leb l1 l2 then + else if Nat.leb l1 l2 then iterate_op (Pmov r) (Porr r r) d1 k else iterate_op (Pmvn r) (Pbic r r) d2 k. @@ -190,7 +190,7 @@ Definition addimm (r1 r2: ireg) (n: int) (k: code) := else (let d1 := decompose_int n in let d2 := decompose_int (Int.neg n) in - if NPeano.leb (List.length d1) (List.length d2) + if Nat.leb (List.length d1) (List.length d2) then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k). @@ -801,4 +801,3 @@ Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := Definition transf_program (p: Mach.program) : res Asm.program := transform_partial_program transf_fundef p. - |