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/Asmgenproof1.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/Asmgenproof1.v')
| -rw-r--r-- | arm/Asmgenproof1.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 3e222ba4..76a7b080 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -333,11 +333,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). + destruct (Nat.leb l1 1%nat). { (* single mov *) econstructor; split. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } - destruct (NPeano.leb l2 1%nat). + destruct (Nat.leb l2 1%nat). { (* single movn *) econstructor; split. apply exec_straight_one. simpl. rewrite Int.not_involutive. reflexivity. auto. @@ -359,7 +359,7 @@ Proof. rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega. change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by omega. f_equal; omega. } - destruct (NPeano.leb l1 l2). + destruct (Nat.leb l1 l2). { (* mov - orr* *) replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero). apply iterate_op_correct. @@ -390,7 +390,7 @@ Proof. (* sub *) econstructor; split. apply exec_straight_one; simpl; auto. split; intros; Simpl. apply Val.sub_opp_add. - 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)))). (* add - add* *) replace (Val.add (rs r2) (Vint n)) with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)). @@ -1498,5 +1498,3 @@ Proof. Qed. End CONSTRUCTORS. - - |