From d7732dcb074392e81c4c5a26cd05c4da313b4a7c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 11 Jan 2021 20:21:59 +0100
Subject: [PATCH] Fix compilation with Coq 8.10 (which has a weaker `lia`).

---
 theories/list_numbers.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 8fe24c17..2d8d2b3d 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -148,7 +148,8 @@ Section seqZ.
   Proof.
     intros. unfold seqZ. rewrite Z2Nat.inj_add, seq_app, fmap_app by done.
     f_equal. rewrite Nat.add_comm, <-!fmap_add_seq, <-list_fmap_compose.
-    apply list_fmap_ext; naive_solver auto with lia.
+    apply list_fmap_ext; [|done]; intros j; simpl.
+    rewrite Nat2Z.inj_add, Z2Nat.id by done. lia.
   Qed.
 
   Lemma seqZ_S m i : seqZ m (S i) = seqZ m i ++ [m + i].
@@ -162,7 +163,7 @@ Section seqZ.
   Proof.
     rewrite elem_of_list_lookup.
     setoid_rewrite lookup_seqZ. split; [naive_solver lia|].
-    exists (Z.to_nat (k - m)). lia.
+    exists (Z.to_nat (k - m)). rewrite Z2Nat.id by lia. lia.
   Qed.
 
   Lemma Forall_seqZ (P : Z → Prop) m n :
-- 
GitLab