Remove coq warnings (#28)

Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.

8 files changed, 50 insertions, 50 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index a9ffcd3d..15818317 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -1769,7 +1769,7 @@ Lemma not_stuckred_imm_safe:
 Proof.
   intros. generalize (step_expr_sound a k m). intros [A B].
   destruct (step_expr k a m) as [|[C rd] res] eqn:?.
-  specialize (B (refl_equal _)). destruct k.
+  specialize (B (eq_refl _)). destruct k.
   destruct a; simpl in B; try congruence. constructor.
   destruct a; simpl in B; try congruence. constructor.
   assert (NOTSTUCK: rd <> Stuckred).
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 5017fc8e..45c21f96 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -226,7 +226,7 @@ Definition assign_variable
   let (id, sz) := id_sz in
   let (cenv, stacksize) := cenv_stacksize in
   let ofs := align stacksize (block_alignment sz) in
-  (PTree.set id ofs cenv, ofs + Zmax 0 sz).
+  (PTree.set id ofs cenv, ofs + Z.max 0 sz).
 
 Definition assign_variables (cenv_stacksize: compilenv * Z) (vars: list (ident * Z)) : compilenv * Z :=
   List.fold_left assign_variable vars cenv_stacksize.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index a6d58f17..ffafc5d2 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -96,7 +96,7 @@ Proof.
   intros m1 FR1 FRL.
   transitivity (Mem.load chunk m1 b ofs).
   eapply IHfbl; eauto. intros. eapply H. eauto with coqlib.
-  eapply Mem.load_free; eauto. left. apply sym_not_equal. eapply H. auto with coqlib.
+  eapply Mem.load_free; eauto. left. apply not_eq_sym. eapply H. auto with coqlib.
 Qed.
 
 Lemma perm_freelist:
@@ -775,7 +775,7 @@ Definition cenv_compat (cenv: compilenv) (vars: list (ident * Z)) (tsz: Z) : Pro
       PTree.get id cenv = Some ofs
    /\ Mem.inj_offset_aligned ofs sz
    /\ 0 <= ofs
-   /\ ofs + Zmax 0 sz <= tsz.
+   /\ ofs + Z.max 0 sz <= tsz.
 
 Definition cenv_separated (cenv: compilenv) (vars: list (ident * Z)) : Prop :=
   forall id1 sz1 ofs1 id2 sz2 ofs2,
@@ -901,7 +901,7 @@ Remark assign_variable_incr:
 Proof.
   simpl; intros. inv H.
   generalize (align_le stksz (block_alignment sz) (block_alignment_pos sz)).
-  assert (0 <= Zmax 0 sz). apply Zmax_bound_l. omega.
+  assert (0 <= Z.max 0 sz). apply Zmax_bound_l. omega.
   omega.
 Qed.
 
@@ -914,7 +914,7 @@ Proof.
 Opaque assign_variable.
   destruct a as [id s]. simpl. intros.
   destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1] eqn:?.
-  apply Zle_trans with sz1. eapply assign_variable_incr; eauto. eauto.
+  apply Z.le_trans with sz1. eapply assign_variable_incr; eauto. eauto.
 Transparent assign_variable.
 Qed.
 
@@ -925,8 +925,8 @@ Proof.
   intros; red; intros.
   apply Zdivides_trans with (block_alignment sz).
   unfold align_chunk.  unfold block_alignment.
-  generalize Zone_divide; intro.
-  generalize Zdivide_refl; intro.
+  generalize Z.divide_1_l; intro.
+  generalize Z.divide_refl; intro.
   assert (2 | 4). exists 2; auto.
   assert (2 | 8). exists 4; auto.
   assert (4 | 8). exists 2; auto.
@@ -942,10 +942,10 @@ Qed.
 
 Remark inj_offset_aligned_block':
   forall stacksize sz,
-  Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Zmax 0 sz).
+  Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Z.max 0 sz).
 Proof.
   intros.
-  replace (block_alignment sz) with (block_alignment (Zmax 0 sz)).
+  replace (block_alignment sz) with (block_alignment (Z.max 0 sz)).
   apply inj_offset_aligned_block.
   rewrite Zmax_spec. destruct (zlt sz 0); auto.
   transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. omega.
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 8d6cdb24..036b768b 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -373,15 +373,15 @@ Lemma sizeof_alignof_compat:
   forall env t, naturally_aligned t -> (alignof env t | sizeof env t).
 Proof.
   induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl.
-- apply Zdivide_refl.
-- destruct i; apply Zdivide_refl.
+- apply Z.divide_refl.
+- destruct i; apply Z.divide_refl.
 - exists (8 / Archi.align_int64). unfold Archi.align_int64; destruct Archi.ptr64; reflexivity.
-- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity.
-- apply Zdivide_refl.
+- destruct f. apply Z.divide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity.
+- apply Z.divide_refl.
 - apply Z.divide_mul_l; auto.
-- apply Zdivide_refl.
-- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0.
-- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0.
+- apply Z.divide_refl.
+- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r.
+- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r.
 Qed.
 
 (** ** Size and alignment for composite definitions *)
@@ -435,9 +435,9 @@ Lemma sizeof_struct_incr:
 Proof.
   induction m as [|[id t]]; simpl; intros.
 - omega.
-- apply Zle_trans with (align cur (alignof env t)).
+- apply Z.le_trans with (align cur (alignof env t)).
   apply align_le. apply alignof_pos.
-  apply Zle_trans with (align cur (alignof env t) + sizeof env t).
+  apply Z.le_trans with (align cur (alignof env t) + sizeof env t).
   generalize (sizeof_pos env t); omega.
   apply IHm.
 Qed.
@@ -488,7 +488,7 @@ Proof.
   inv H. inv H0. split.
   apply align_le. apply alignof_pos. apply sizeof_struct_incr.
   exploit IHfld; eauto. intros [A B]. split; auto.
-  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof env t)).
+  eapply Z.le_trans; eauto. apply Z.le_trans with (align pos (alignof env t)).
   apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega.
 Qed.
 
@@ -627,7 +627,7 @@ Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z :=
 Lemma alignof_blockcopy_1248:
   forall env ty, let a := alignof_blockcopy env ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8.
 Proof.
-  assert (X: forall co, let a := Zmin 8 (co_alignof co) in
+  assert (X: forall co, let a := Z.min 8 (co_alignof co) in
              a = 1 \/ a = 2 \/ a = 4 \/ a = 8).
   {
     intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ.
@@ -635,7 +635,7 @@ Proof.
     destruct n; auto.
     destruct n; auto.
     right; right; right. apply Z.min_l.
-    rewrite two_power_nat_two_p. rewrite ! inj_S.
+    rewrite two_power_nat_two_p. rewrite ! Nat2Z.inj_succ.
     change 8 with (two_p 3). apply two_p_monotone. omega.
   }
   induction ty; simpl.
@@ -661,28 +661,28 @@ Lemma sizeof_alignof_blockcopy_compat:
 Proof.
   assert (X: forall co, (Z.min 8 (co_alignof co) | co_sizeof co)).
   {
-    intros. apply Zdivide_trans with (co_alignof co). 2: apply co_sizeof_alignof.
+    intros. apply Z.divide_trans with (co_alignof co). 2: apply co_sizeof_alignof.
     destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ.
-    destruct n. apply Zdivide_refl.
-    destruct n. apply Zdivide_refl.
-    destruct n. apply Zdivide_refl.
+    destruct n. apply Z.divide_refl.
+    destruct n. apply Z.divide_refl.
+    destruct n. apply Z.divide_refl.
     apply Z.min_case.
     exists (two_p (Z.of_nat n)).
     change 8 with (two_p 3).
     rewrite <- two_p_is_exp by omega.
-    rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega.
-    apply Zdivide_refl.
+    rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. omega.
+    apply Z.divide_refl.
   }
   induction ty; simpl.
-  apply Zdivide_refl.
-  apply Zdivide_refl.
-  apply Zdivide_refl.
-  apply Zdivide_refl.
-  apply Zdivide_refl.
+  apply Z.divide_refl.
+  apply Z.divide_refl.
+  apply Z.divide_refl.
+  apply Z.divide_refl.
+  apply Z.divide_refl.
   apply Z.divide_mul_l. auto.
-  apply Zdivide_refl.
-  destruct (env!i). apply X. apply Zdivide_0.
-  destruct (env!i). apply X. apply Zdivide_0.
+  apply Z.divide_refl.
+  destruct (env!i). apply X. apply Z.divide_0_r.
+  destruct (env!i). apply X. apply Z.divide_0_r.
 Qed.
 
 (** Type ranks *)
@@ -707,7 +707,7 @@ Fixpoint rank_type (ce: composite_env) (t: type) : nat :=
 Fixpoint rank_members (ce: composite_env) (m: members) : nat :=
   match m with
   | nil => 0%nat
-  | (id, t) :: m => Peano.max (rank_type ce t) (rank_members ce m)
+  | (id, t) :: m => Init.Nat.max (rank_type ce t) (rank_members ce m)
   end.
 
 (** ** C types and back-end types *)
@@ -818,7 +818,7 @@ Program Definition composite_of_def
             co_sizeof_alignof := _ |}
   end.
 Next Obligation.
-  apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos.
+  apply Z.le_ge. eapply Z.le_trans. eapply sizeof_composite_pos.
   apply align_le; apply alignof_composite_pos.
 Defined.
 Next Obligation.
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 388b6544..77d6cfea 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -186,7 +186,7 @@ Fixpoint transl_init_rec (ce: composite_env) (ty: type) (i: initializer)
   | Init_single a, _ =>
       do d <- transl_init_single ce ty a; OK (d :: k)
   | Init_array il, Tarray tyelt nelt _ =>
-      transl_init_array ce tyelt il (Zmax 0 nelt) k
+      transl_init_array ce tyelt il (Z.max 0 nelt) k
   | Init_struct il, Tstruct id _ =>
       do co <- lookup_composite ce id;
       match co_su co with
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 524bc631..272b929f 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -486,7 +486,7 @@ Inductive tr_init: type -> initializer -> list init_data -> Prop :=
       transl_init_single ge ty a = OK d ->
       tr_init ty (Init_single a) (d :: nil)
   | tr_init_arr: forall tyelt nelt attr il d,
-      tr_init_array tyelt il (Zmax 0 nelt) d ->
+      tr_init_array tyelt il (Z.max 0 nelt) d ->
       tr_init (Tarray tyelt nelt attr) (Init_array il) d
   | tr_init_str: forall id attr il co d,
       lookup_composite ge id = OK co -> co_su co = Struct ->
@@ -723,7 +723,7 @@ Local Opaque sizeof.
 + rewrite idlsize_app, padding_size. 
   exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega.
   simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H.
-  apply Zle_trans with (sizeof_union ge (co_members co)).
+  apply Z.le_trans with (sizeof_union ge (co_members co)).
   eapply union_field_size; eauto.
   erewrite co_consistent_sizeof by (eapply ce_consistent; eauto).
   unfold sizeof_composite. rewrite H0. apply align_le.
@@ -816,9 +816,9 @@ Lemma store_init_data_list_app:
   Genv.store_init_data_list ge m b ofs (data1 ++ data2) = Some m''.
 Proof.
   induction data1; simpl; intros.
-  inv H. rewrite Zplus_0_r in H0. auto.
+  inv H. rewrite Z.add_0_r in H0. auto.
   destruct (Genv.store_init_data ge m b ofs a); try discriminate.
-  rewrite Zplus_assoc in H0. eauto.
+  rewrite Z.add_assoc in H0. eauto.
 Qed.
 
 Remark store_init_data_list_padding:
@@ -874,7 +874,7 @@ Local Opaque sizeof.
   eapply store_init_data_list_app.
   eauto.
   rewrite (tr_init_size _ _ _ H9).
-  rewrite <- Zplus_assoc. eapply H2. eauto. eauto.
+  rewrite <- Z.add_assoc. eapply H2. eauto. eauto.
   apply align_le. apply alignof_pos.
 Qed.
 
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 0a191f29..45b686f3 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -80,7 +80,7 @@ Definition initial_generator (x: unit) : generator :=
 Definition gensym (ty: type): mon ident :=
   fun (g: generator) =>
     Res (gen_next g)
-        (mkgenerator (Psucc (gen_next g)) ((gen_next g, ty) :: gen_trail g))
+        (mkgenerator (Pos.succ (gen_next g)) ((gen_next g, ty) :: gen_trail g))
         (Ple_succ (gen_next g)).
 
 (** Construct a sequence from a list of statements.  To facilitate the
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 8ed924e5..7af499f4 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -604,7 +604,7 @@ Proof.
   destruct (peq id id0). inv A.
   right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto.
   generalize (alloc_variables_nextblock _ _ _ _ _ _ H0). intros A B C.
-  subst b. split. apply Ple_refl. eapply Plt_le_trans; eauto. rewrite B. apply Plt_succ.
+  subst b. split. apply Ple_refl. eapply Pos.lt_le_trans; eauto. rewrite B. apply Plt_succ.
   auto.
   right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. xomega.
 Qed.
@@ -696,7 +696,7 @@ Proof.
 
   (* variable is not lifted out of memory *)
   exploit Mem.alloc_parallel_inject.
-    eauto. eauto. apply Zle_refl. apply Zle_refl.
+    eauto. eauto. apply Z.le_refl. apply Z.le_refl.
   intros [j1 [tm1 [tb1 [A [B [C [D E]]]]]]].
   exploit IHalloc_variables; eauto. instantiate (1 := PTree.set id (tb1, ty) te).
   intros [j' [te' [tm' [J [K [L [M [N [Q [O P]]]]]]]]]].
@@ -778,8 +778,8 @@ Proof.
   apply IHalloc_variables. red; intros. rewrite PTree.gsspec in H2.
   destruct (peq id0 id). inv H2.
   eapply Mem.load_alloc_same'; eauto.
-  omega. rewrite Zplus_0_l. eapply sizeof_by_value; eauto.
-  apply Zdivide_0.
+  omega. rewrite Z.add_0_l. eapply sizeof_by_value; eauto.
+  apply Z.divide_0_r.
   eapply Mem.load_alloc_other; eauto.
 Qed.
 
@@ -1053,7 +1053,7 @@ Proof.
   assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty).
     eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
   assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty).
-    replace (sizeof tge ty) with (Z_of_nat (length bytes)).
+    replace (sizeof tge ty) with (Z.of_nat (length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
     rewrite LEN. apply nat_of_Z_eq. omega.
   assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty).