diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-03-06 16:37:07 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-03-10 18:53:48 +0100 |
| commit | 2c2dabd4f7b7f330cc8e6c9cf879618a422316e8 (patch) | |
| tree | 21b0faabd86aac8fde4953b926ae5281221a0b89 /common/Memdata.v | |
| parent | 1a7b93078eb531a6e9e5d4dc02bec143605c2264 (diff) | |
| download | compcert-2c2dabd4f7b7f330cc8e6c9cf879618a422316e8.tar.gz compcert-2c2dabd4f7b7f330cc8e6c9cf879618a422316e8.zip | |
Address most deprecation warnings from Coq 8.16
* Define our own `Z_div_mod_eq` lemma
The one in the Coq standard library is deprecated since 8.14,
but its replacement changed type between 8.13 and 8.14.
So the only way to remain compatible from 8.12 to 8.16 is to define our
own lemma. Phew.
* Do not use `Arith.Max`, deprecated.
* Do not use `plus_lt_compat_r`, deprecated.
* Do not use `beq_nat_refl` and `beq_nat_true`, deprecated.
Diffstat (limited to 'common/Memdata.v')
| -rw-r--r-- | common/Memdata.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index 1bd87169..7622cab3 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -426,7 +426,7 @@ Lemma check_inj_value: Proof. induction n; simpl. auto. unfold proj_sumbool. rewrite dec_eq_true. rewrite dec_eq_true. - rewrite <- beq_nat_refl. simpl; auto. + rewrite Nat.eqb_refl. simpl; auto. Qed. Lemma proj_inj_value: @@ -719,7 +719,7 @@ Proof. { induction n; destruct mvs; simpl; intros; try discriminate. contradiction. - destruct m; try discriminate. InvBooleans. apply beq_nat_true in H4. subst. + destruct m; try discriminate. InvBooleans. apply Nat.eqb_eq in H4. subst. destruct H0. subst mv. exists n0; split; auto. lia. eapply IHn; eauto. lia. } @@ -738,7 +738,7 @@ Proof. destruct (quantity_eq q q0); auto. destruct (Nat.eqb sz n) eqn:EQN; auto. destruct (check_value sz v q mvl) eqn:CHECK; auto. - simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto. + simpl. apply Nat.eqb_eq in EQN. subst n q0. constructor. auto. destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate. congruence. intros. eapply B; eauto. lia. @@ -797,9 +797,9 @@ Lemma check_value_inject: Proof. induction 1; intros; destruct n; simpl in *; auto. inv H; auto. - InvBooleans. assert (n = n0) by (apply beq_nat_true; auto). subst v1 q0 n0. + InvBooleans. assert (n = n0) by (apply Nat.eqb_eq; auto). subst v1 q0 n0. replace v2 with v'. - unfold proj_sumbool; rewrite ! dec_eq_true. rewrite <- beq_nat_refl. simpl; eauto. + unfold proj_sumbool; rewrite ! dec_eq_true. rewrite Nat.eqb_refl. simpl; eauto. inv H2; try discriminate; inv H4; congruence. discriminate. Qed. |