Port to Coq 8.5pl2

Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.

4 files changed, 14 insertions, 17 deletions

diff --git a/arm/Archi.v b/arm/Archi.v
index e4abf009..6b282022 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -26,7 +26,7 @@ Notation align_int64 := 8%Z (only parsing).
 Notation align_float64 := 8%Z (only parsing).
 
 Program Definition default_pl_64 : bool * nan_pl 53 :=
-  (false, nat_iter 51 xO xH).
+  (false, iter_nat 51 _ xO xH).
 
 Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
   (** Choose second NaN if pl2 is sNaN but pl1 is qNan.
@@ -35,7 +35,7 @@ Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_p
    negb (Pos.testbit (proj1_sig pl2) 51))%bool.
 
 Program Definition default_pl_32 : bool * nan_pl 24 :=
-  (false, nat_iter 22 xO xH).
+  (false, iter_nat 22 _ xO xH).
 
 Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) :=
   (** Choose second NaN if pl2 is sNaN but pl1 is qNan.
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.
-
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.
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.
-
-