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 /cfrontend | |
| 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 'cfrontend')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 2aed0cdf..04afe4da 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1974,7 +1974,7 @@ Ltac NOTIN := exploit tr_simple_rvalue; eauto. simpl; intro SL1. subst sl0; simpl Kseqlist. econstructor; split. - right; split. apply star_refl. simpl. apply plus_lt_compat_r. + right; split. apply star_refl. simpl. apply Nat.add_lt_mono_r. apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. apply S. eapply tr_expr_monotone; eauto. @@ -1996,7 +1996,7 @@ Ltac NOTIN := auto. + (* for effects *) econstructor; split. - right; split. apply star_refl. simpl. apply plus_lt_compat_r. + right; split. apply star_refl. simpl. apply Nat.add_lt_mono_r. apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. exploit tr_simple_rvalue; eauto. simpl. intros A. subst sl1. |