From 5e0eed6a061f05ee38cc1b9d24d65ffeb8cee54c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 23 Mar 2023 23:10:04 +0100
Subject: [PATCH] hopefully make proof work under older Coq

---
 stdpp/listZ.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/stdpp/listZ.v b/stdpp/listZ.v
index 3c6bf20c..a5ec05ea 100644
--- a/stdpp/listZ.v
+++ b/stdpp/listZ.v
@@ -123,9 +123,9 @@ Lemma lookupZ_app l1 l2 i :
     match l1 !! i with Some x => Some x | None => l2 !! (i - lengthZ l1) end.
 Proof.
   rewrite !lookupZ_eq. Z.case_to_onat; simpl.
-  - rewrite lookup_app. case_match. 1:done.
+  - rewrite lookup_app. case_match eqn:Hli. 1:done.
     assert (lengthZ l1 ≤ i).
-    { rewrite lookup_ge_None in *. lia. }
+    { apply lookup_ge_None in Hli. lia. }
     rewrite Z.to_onat_nonneg by lia. simpl. f_equal. lia.
   - rewrite Z.to_onat_neg by lia. done.
 Qed.
-- 
GitLab