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/Switch.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/Switch.v')
| -rw-r--r-- | common/Switch.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/common/Switch.v b/common/Switch.v index 70d1da15..23f9dd3e 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -271,7 +271,7 @@ Lemma validate_jumptable_correct_rec: Proof. induction tbl; simpl; intros. - unfold list_length_z in H0. simpl in H0. extlia. -- InvBooleans. rewrite list_length_z_cons in H0. apply beq_nat_true in H1. +- InvBooleans. rewrite list_length_z_cons in H0. apply Nat.eqb_eq in H1. destruct (zeq v 0). + replace (base + v) with base by lia. congruence. + replace (base + v) with (Z.succ base + Z.pred v) by lia. @@ -308,13 +308,13 @@ Proof. intros default v VRANGE. induction t; simpl; intros until hi. - (* base case *) destruct cases as [ | [key1 act1] cases1]; intros. -+ apply beq_nat_true in H. subst act. reflexivity. -+ InvBooleans. apply beq_nat_true in H2. subst. simpl. ++ apply Nat.eqb_eq in H. subst act. reflexivity. ++ InvBooleans. apply Nat.eqb_eq in H2. subst. simpl. destruct (zeq v hi). auto. extlia. - (* eq node *) destruct (split_eq key cases) as [optact others] eqn:EQ. intros. destruct optact as [act1|]; InvBooleans; try discriminate. - apply beq_nat_true in H. + apply Nat.eqb_eq in H. rewrite (split_eq_prop v default _ _ _ _ EQ). destruct (zeq v key). + congruence. |