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/Iteration.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/Iteration.v')
| -rw-r--r-- | lib/Iteration.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/lib/Iteration.v b/lib/Iteration.v index 34471826..50672069 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -204,7 +204,6 @@ End PrimIter. Require Import Classical. Require Import ClassicalDescription. -Require Import Max. Module GenIter. @@ -280,7 +279,7 @@ Lemma converges_to_unique: Proof. intros a b [n C] b' [n' C']. rewrite <- (C (max n n')). rewrite <- (C' (max n n')). auto. - apply le_max_r. apply le_max_l. + apply Nat.le_max_r. apply Nat.le_max_l. Qed. Lemma converges_to_exists_uniquely: |