From 2db35c481b1b32ff2902201bbec715b5aa6c3257 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Sep 2024 18:29:34 +0200
Subject: [PATCH] Unsilence deprecation warning regarding list lemmas.

---
 _CoqProject  | 2 --
 stdpp/list.v | 5 ++++-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 723a4beb..40d93206 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,8 +7,6 @@
 # Custom flags (to be kept in sync with the dune file at the root of the repo).
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
-# Fixing this requires Coq 8.20.
--arg -w -arg -deprecated-since-8.20
 # https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
 -arg -w -arg -notation-incompatible-prefix
 
diff --git a/stdpp/list.v b/stdpp/list.v
index cc68e906..9b25e6d9 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -881,7 +881,10 @@ Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
 Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
 Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
 Lemma length_reverse l : length (reverse l) = length l.
-Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
+Proof.
+  induction l as [|x l IH]; [done|].
+  rewrite reverse_cons, length_app, IH. simpl. lia.
+Qed.
 Lemma reverse_involutive l : reverse (reverse l) = l.
 Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
 Lemma reverse_lookup l i :
-- 
GitLab