diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-22 19:53:06 +0200 |
| commit | 8d5c6bb8f0cac1339dec7b730997ee30b1517073 (patch) | |
| tree | 3ffd8bcb28a88ae4ff51989aed37b0ad2cb676b2 /powerpc/Asmgenproof1.v | |
| parent | 0f210f622a4609811959f4450f770c61f5eb6532 (diff) | |
| download | compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.tar.gz compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.zip | |
Remove coq warnings (#28)
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
Diffstat (limited to 'powerpc/Asmgenproof1.v')
| -rw-r--r-- | powerpc/Asmgenproof1.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index e5736277..460fa670 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -39,9 +39,9 @@ Proof. intros. unfold high_u, low_u. rewrite Int.shl_rolm. rewrite Int.shru_rolm. rewrite Int.rolm_rolm. - change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16)) + change (Int.modu (Int.add (Int.sub (Int.repr (Z.of_nat Int.wordsize)) (Int.repr 16)) (Int.repr 16)) - (Int.repr (Z_of_nat Int.wordsize))) + (Int.repr (Z.of_nat Int.wordsize))) with (Int.zero). rewrite Int.rolm_zero. rewrite <- Int.and_or_distrib. exact (Int.and_mone n). @@ -54,9 +54,9 @@ Proof. intros. unfold high_u, low_u. rewrite Int.shl_rolm. rewrite Int.shru_rolm. rewrite Int.rolm_rolm. - change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16)) + change (Int.modu (Int.add (Int.sub (Int.repr (Z.of_nat Int.wordsize)) (Int.repr 16)) (Int.repr 16)) - (Int.repr (Z_of_nat Int.wordsize))) + (Int.repr (Z.of_nat Int.wordsize))) with (Int.zero). rewrite Int.rolm_zero. rewrite <- Int.and_xor_distrib. exact (Int.and_mone n). @@ -198,7 +198,7 @@ Hint Resolve ireg_of_not_GPR0': asmgen. Lemma preg_of_not_LR: forall r, LR <> preg_of r. Proof. - intros. auto using sym_not_equal with asmgen. + intros. auto using not_eq_sym with asmgen. Qed. Lemma preg_notin_LR: @@ -1243,7 +1243,7 @@ Opaque Val.add. econstructor; split. eapply exec_straight_trans. eapply exec_straight_two; simpl; reflexivity. eapply exec_straight_two; simpl; reflexivity. - split. assert (GPR0 <> x0) by (apply sym_not_equal; eauto with asmgen). + split. assert (GPR0 <> x0) by (apply not_eq_sym; eauto with asmgen). Simpl. rewrite ! gpr_or_zero_zero. rewrite ! gpr_or_zero_not_zero by eauto with asmgen. Simpl. rewrite low_high_half_zero. auto. intros; Simpl. |