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 /lib/Coqlib.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 'lib/Coqlib.v')
| -rw-r--r-- | lib/Coqlib.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 045fb03a..9b8f2abb 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -406,6 +406,12 @@ Qed. (** Properties of Euclidean division and modulus. *) +Lemma Z_div_mod_eq: forall a b, + b > 0 -> a = (b * (a / b) + a mod b). +Proof. + intros. apply Z.div_mod. lia. +Qed. + Lemma Zmod_unique: forall x y a b, x = a * y + b -> 0 <= b < y -> x mod y = b. |